Theorem 3expa 1116

Description: Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.) (Revised to shorten 3exp 1117 and pm3.2an3 1338 by Wolf Lammen, 22-Jun-2022.)

Hypothesis

Ref	Expression
3exp.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3expa	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Proof of Theorem 3expa

Step	Hyp	Ref	Expression
1		df-3an 1087	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		3exp.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	1, 2	sylbir 234	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-3an 1087

This theorem is referenced by:  3exp  1117  ad4ant123  1170  ad4ant124  1171  ad4ant134  1172  ad4ant234  1173  ad5ant123  1362  3anidm23  1419  mp3an2  1446  mpd3an3  1459  rgen3  3197  vtocl3  3551  spc3egv  3588  moi2  3709  sbc3ie  3859  2if2  4579  preq12bg  4850  ralxfrd2  5406  reuhypd  5413  otsndisj  5515  funcnvqp  6611  fvtp1g  7204  fntpb  7215  f1imass  7268  weisoeq  7357  f1ofveu  7408  f1ocnvfv3  7409  funeldmdif  8046  curry1f  8105  curry2f  8107  funsssuppss  8188  frrlem13  8297  tfrlem11  8402  oalimcl  8574  oeordsuc  8608  oelim2  8609  nneob  8670  nadd4  8712  mapxpen  9159  findcard  9179  enfii  9205  domtrfil  9211  domnsymfi  9219  phplem2  9224  php  9226  wemaplem3  9563  en2eqpr  10022  infxpabs  10227  infxp  10230  cfflb  10274  cfsmolem  10285  isf32lem12  10379  fin1a2lem9  10423  fin1a2s  10429  axcc3  10453  axdc3lem4  10468  zornn0g  10520  pwfseqlem4  10677  tskwun  10799  tskint  10800  tskxp  10802  tskmap  10803  gruf  10826  grutsk1  10836  addcanpi  10914  ltapi  10918  mul4  11404  add4  11456  2addsub  11496  addsubeq4  11497  muladd  11668  ltleadd  11719  receu  11881  p1le  12081  lbinf  12189  zdiv  12654  fzind  12682  fnn0ind  12683  fzindd  12686  uzss  12867  zbtwnre  12952  qmulcl  12973  qreccl  12975  xrlttr  13143  xaddass  13252  xmulasslem3  13289  xadddilem  13297  xrsupsslem  13310  xrinfmsslem  13311  supxrunb1  13322  ioo0  13373  ico0  13394  ioc0  13395  icc0  13396  iooshf  13427  prunioo  13482  ioojoin  13484  elfz5  13517  elfz0fzfz0  13630  elfzonelfzo  13758  fzind2  13774  mulexpz  14091  expsub  14099  digit1  14223  facndiv  14271  faclbnd4lem4  14279  faclbnd4  14280  faclbnd5  14281  bccmpl  14292  bcval5  14301  bcpasc  14304  hashunx  14369  hashunsnggt  14377  hashdmpropge2  14468  ccatrn  14563  swrdspsleq  14639  swrdccat2  14643  ccatpfx  14675  pfxccat1  14676  swrdswrd  14679  cshf1  14784  crim  15086  absmax  15300  ello12r  15485  elo12r  15496  climshftlem  15542  2sumeq2dv  15675  hash2iun  15793  expcnv  15834  2cprodeq2dv  15893  rpnnen2lem7  16188  dvdsval3  16226  dvdsnegb  16242  muldvds1  16249  muldvds2  16250  dvdscmul  16251  dvdsmulc  16252  dvdsmulcr  16254  dvds2ln  16257  divalgb  16372  ndvdssub  16377  gcddiv  16518  lcmfval  16583  lcmfcl  16590  dvdslcmf  16593  rpexp1i  16686  phiprmpw  16736  hashgcdeq  16749  pythagtriplem1  16776  pockthg  16866  infpnlem1  16870  4sqlem3  16910  0ramcl  16983  firest  17405  imasaddfnlem  17501  imasleval  17514  mrerintcl  17568  iscatd  17644  fullestrcsetc  18133  fullsetcestrc  18148  clatleglb  18501  mreclatBAD  18546  pslem  18555  mndind  18771  grplmulf1o  18960  grplactcnv  18990  mulgnn0subcl  19033  mulgsubcl  19034  mulgdir  19052  issubg2  19087  issubgrpd2  19088  nmzsubg  19111  eqgen  19127  cycsubm  19148  cycsubgcl  19152  cycsubgss  19153  ghmmulg  19173  ghmf1  19191  kerf1ghm  19192  conjghm  19194  symgpssefmnd  19341  gsmsymgreqlem2  19377  symgfixfo  19385  odeq  19496  odval2  19497  odf1  19508  dfod2  19510  gexdvds  19530  gexdvds2  19531  gexcl2  19535  gexdvds3  19536  sylow2blem2  19567  efgsp1  19683  efgrelexlemb  19696  cmnbascntr  19751  mulgmhm  19773  mulgghm  19774  iscyggen2  19827  iscyg3  19832  ablsimpgfindlem1  20055  srglmhm  20152  srgrmhm  20153  ringlghm  20237  ringrghm  20238  gsumdixp  20244  dvdsrcl2  20294  crngunit  20306  cntzsubrng  20493  subrgugrp  20519  cntzsubr  20534  rnghmsubcsetclem2  20554  rhmsubcsetclem2  20583  rhmsubcrngclem2  20589  sdrgacs  20678  lmodvsdir  20758  lmodvsass  20759  lmodvsghm  20795  lsssubg  20830  lss1d  20836  islbs2  21031  lidlsubg  21108  lidlsubcl  21109  rngqiprngimfo  21180  lpigen  21214  xrsdsreval  21331  expghm  21388  mulgghm2  21389  ip0r  21556  obs2ss  21650  islindf3  21747  scmatscm  22402  scmataddcl  22405  scmatsubcl  22406  scmatfo  22419  matunit  22567  cpmatelimp  22601  cpmatelimp2  22603  cpmatinvcl  22606  cpmatmcl  22608  mat2pmatf  22617  m2cpmf  22631  cpm2mf  22641  m2cpmfo  22645  m2cpminv  22649  decpmataa0  22657  pm2mpf  22687  pm2mpf1  22688  idpm2idmp  22690  pm2mpfo  22703  elcls2  22965  opnnei  23011  innei  23016  iscnp4  23154  cnpnei  23155  iscncl  23160  cnnei  23173  cnconst  23175  ordthauslem  23274  bwth  23301  1stccnp  23353  llyrest  23376  nllyrest  23377  kgenss  23434  xkoccn  23510  kqsat  23622  kqt0lem  23627  isr0  23628  fbssfi  23728  isfild  23749  filconn  23774  trfilss  23780  fgtr  23781  ufileu  23810  ufilen  23821  fmfnfmlem4  23848  fmfnfm  23849  hausflimi  23871  cnpflf2  23891  cnpflf  23892  cnpfcf  23932  cnextcn  23958  tsmsxplem1  24044  tsmsxp  24046  ustuqtop0  24132  ismeti  24218  isxmet2d  24220  elbl2ps  24282  elbl2  24283  xblpnfps  24288  xblpnf  24289  xbln0  24307  blin  24314  blssexps  24319  blssex  24320  blcls  24402  blsscls  24403  metrest  24420  metustbl  24462  psmetutop  24463  nmf2  24489  ngpi  24524  tngngp3  24560  nmdvr  24574  nmoi  24632  nmoix  24633  nmoleub  24635  nghmcn  24649  iccntr  24724  metdsle  24755  icoopnst  24850  iocopnst  24851  icccvx  24862  pi1xfr  24969  isclmi0  25012  iscvsi  25043  cphipval  25158  lmmbr  25173  lmmbr2  25174  iscfil3  25188  iscau2  25192  cfilres  25211  bcthlem1  25239  bcthlem4  25242  bcthlem5  25243  rrxmet  25323  ioombl  25481  iccvolcl  25483  ioovolcl  25486  mbfi1fseqlem3  25634  mbfi1fseqlem4  25635  mbfi1fseqlem5  25636  ig1pcl  26100  ig1prsp  26102  aannenlem1  26250  taylplem1  26284  dvtaylp  26292  relogeftb  26505  logdivlt  26542  cxpexp  26589  rpcxpcl  26597  isppw2  27034  vmappw  27035  lgslem4  27220  lgscllem  27224  lgsneg1  27242  lgsne0  27255  nosepdm  27604  ssltdisj  27741  mulscutlem  28018  sltonold  28140  brbtwn2  28703  ax5seglem1  28726  ax5seglem2  28727  axcontlem4  28765  ewlkprop  29404  uspgr2wlkeq  29447  uhgrwkspthlem2  29555  clwlkclwwlkfo  29806  eupth2lem3lem7  30031  frgr3vlem2  30071  3cyclfrgrrn1  30082  4cycl2vnunb  30087  frgrncvvdeqlem8  30103  grpoidinvlem3  30303  isvciOLD  30377  nmcvcn  30492  ipval2lem2  30501  sspimsval  30535  isblo2  30580  nmoo0  30588  blocni  30602  isph  30619  hvadd4  30833  hiassdi  30888  ocsh  31080  chj4  31332  spansncol  31365  pjjsi  31497  hoscl  31542  hodcl  31544  hoadd4  31581  homco1  31598  homulass  31599  hoadddi  31600  hoadddir  31601  unoplin  31717  adjvalval  31734  hmoplin  31739  bralnfn  31745  brafnmul  31748  lnopmi  31797  lnopcoi  31800  hmops  31817  hmopm  31818  nmophmi  31828  lnfncnbd  31854  cnlnadjlem2  31865  adjlnop  31883  adjmul  31889  adjadd  31890  branmfn  31902  kbass5  31917  kbass6  31918  leop2  31921  leopadd  31929  leopmuli  31930  pjimai  31973  atcvatlem  32182  chirredlem2  32188  mdsymlem3  32202  mdsymlem5  32204  sumdmdii  32212  sumdmdlem  32215  cdj3lem2a  32233  cdj3lem2b  32234  cdj3lem3a  32236  cdj3i  32238  nn0difffzod  32557  xreceu  32627  cshwrnid  32664  toslublem  32681  tosglblem  32683  lmodvslmhm  32742  ogrpaddltbi  32776  archiabllem1b  32878  archiabllem2c  32881  archiabl  32884  slmdvsdir  32901  slmdvsass  32902  grplsm0l  33052  pidlnzb  33073  zarcls1  33406  pstmxmet  33434  ordtconnlem1  33461  hasheuni  33640  omsf  33852  ballotlemirc  34087  signswmnd  34125  bnj1204  34579  fineqvac  34653  fisshasheq  34660  revpfxsfxrev  34661  txpconn  34778  cvmscld  34819  satfbrsuc  34912  satfrnmapom  34916  satfun  34957  elmpps  35119  dfrdg2  35327  wsuclem  35357  segconeu  35543  linecom  35682  linethru  35685  lineintmo  35689  fnemeet2  35787  fnejoin2  35789  fvineqsneq  36827  lindsadd  37021  lindsdom  37022  lindsenlbs  37023  matunitlindflem1  37024  matunitlindflem2  37025  heicant  37063  mblfinlem1  37065  mblfinlem3  37067  ismblfin  37069  cnambfre  37076  itg2addnclem2  37080  ftc1anclem1  37101  ftc1anclem5  37105  ftc1anclem6  37106  ftc2nc  37110  areacirclem2  37117  areacirclem4  37119  areacirclem5  37120  areacirc  37121  fzmul  37149  subspopn  37160  isbndx  37190  isbnd2  37191  isbnd3  37192  ssbnd  37196  prdstotbnd  37202  heibor1  37218  rrnmet  37237  rngonegmn1l  37349  rngohomco  37382  rngoisocnv  37389  rngoisoco  37390  crngohomfo  37414  isidlc  37423  rngoidl  37432  prnc  37475  ispridlc  37478  cvrval2  38683  glbconxN  38788  hlrelat5N  38811  cvratlem  38831  cvrat2  38839  athgt  38866  3dim2  38878  llnn0  38926  lplnn0N  38957  lvoln0N  39001  snatpsubN  39160  paddasslem18  39247  pmod1i  39258  lhpexle2  39420  lhpexle3lem  39421  lhpexle3  39422  ldilcnv  39525  trlcnv  39575  trlnidatb  39587  cdleme32snaw  39845  cdleme32fvaw  39849  cdleme42ke  39895  cdlemeg46gf  39943  cdleme50trn12  39962  cdlemg1cex  39998  cdlemb3  40016  tgrpgrplem  40159  tgrpabl  40161  tendoplcl2  40188  tendo0pl  40201  tendoicl  40206  tendoipl  40207  cdlemkid3N  40343  tendoex  40385  erngdvlem4  40401  erngdvlem4-rN  40409  dib1dim  40575  dib1dim2  40578  dihglbcpreN  40710  dihmeetALTN  40737  dih1dimatlem  40739  dihatlat  40744  lcmineqlem1  41437  lcmineqlem3  41439  aks4d1p1  41484  aks4d1p7d1  41490  aks4d1p8  41495  sticksstones1  41550  sticksstones2  41551  sticksstones3  41552  sticksstones8  41557  sticksstones10  41559  sticksstones11  41560  sticksstones12a  41561  sticksstones12  41562  sticksstones17  41567  sticksstones19  41569  metakunt29  41605  metakunt30  41606  metakunt31  41607  factwoffsmonot  41614  oddcomabszz  42287  acongtr  42321  rpnnen3lem  42374  islssfg  42416  lmhmfgsplit  42432  unxpwdom3  42441  hbtlem7  42471  iocmbl  42564  ss2iundf  43012  ismnu  43621  grumnudlem  43645  ismnushort  43661  nzss  43677  dvconstbi  43694  bccbc  43705  uzmptshftfval  43706  iccdifprioo  44824  climisp  45057  limsupresxr  45077  liminfresxr  45078  dvnmul  45254  volico  45294  volioore  45301  fourierdlem74  45491  fourierdlem75  45492  sge0iunmptlemfi  45724  sge0iunmptlemre  45726  sge0iunmpt  45729  sge0xp  45740  hspmbllem2  45938  smflimlem3  46084  smfsupmpt  46126  smfinflem  46128  smfinfmpt  46130  smflimsupmpt  46140  smfliminfmpt  46143  funressnbrafv2  46547  uniimaelsetpreimafv  46659  imasetpreimafvbijlemfv1  46666  imasetpreimafvbijlemfo  46668  sprsymrelfo  46760  nnsum4primesodd  47059  nnsum4primesoddALTV  47060  uspgrimprop  47094  nn0mnd  47164  lcoss  47427  snlindsntorlem  47461  mreclat  47931  aacllem  48157