Theorem 3expa 1120

Description: Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.) (Revised to shorten 3exp 1121 and pm3.2an3 1342 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 1091	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		3exp.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	1, 2	sylbir 238	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1089

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 210  df-3an 1091

This theorem is referenced by:  3exp  1121  ad4ant123  1174  ad4ant124  1175  ad4ant134  1176  ad4ant234  1177  ad5ant123  1366  3anidm23  1423  mp3an2  1451  mpd3an3  1464  rgen3  3115  vtocl3  3467  spc3egv  3508  moi2  3618  sbc3ie  3768  2if2  4480  preq12bg  4750  ralxfrd2  5290  reuhypd  5297  otsndisj  5387  funcnvqp  6422  fvtp1g  6991  fntpb  7003  f1imass  7054  weisoeq  7142  f1ofveu  7186  f1ocnvfv3  7187  funeldmdif  7797  curry1f  7852  curry2f  7854  funsssuppss  7910  frrlem13  8017  tfrlem11  8102  oalimcl  8266  oeordsuc  8300  oelim2  8301  nneob  8359  mapxpen  8790  findcard  8819  enfii  8841  wemaplem3  9142  en2eqpr  9586  infxpabs  9791  infxp  9794  cfflb  9838  cfsmolem  9849  isf32lem12  9943  fin1a2lem9  9987  fin1a2s  9993  axcc3  10017  axdc3lem4  10032  zornn0g  10084  pwfseqlem4  10241  tskwun  10363  tskint  10364  tskxp  10366  tskmap  10367  gruf  10390  grutsk1  10400  addcanpi  10478  ltapi  10482  mul4  10965  add4  11017  2addsub  11057  addsubeq4  11058  muladd  11229  ltleadd  11280  receu  11442  p1le  11642  lbinf  11750  zdiv  12212  fzind  12240  fnn0ind  12241  uzss  12426  zbtwnre  12507  qmulcl  12528  qreccl  12530  xrlttr  12695  xaddass  12804  xmulasslem3  12841  xadddilem  12849  xrsupsslem  12862  xrinfmsslem  12863  supxrunb1  12874  ioo0  12925  ico0  12946  ioc0  12947  icc0  12948  iooshf  12979  prunioo  13034  ioojoin  13036  elfz5  13069  elfz0fzfz0  13182  elfzonelfzo  13309  fzind2  13325  mulexpz  13640  expsub  13648  digit1  13769  facndiv  13819  faclbnd4lem4  13827  faclbnd4  13828  faclbnd5  13829  bccmpl  13840  bcval5  13849  bcpasc  13852  hashunx  13918  hashunsnggt  13926  hashdmpropge2  14014  ccatrn  14111  swrdspsleq  14195  swrdccat2  14199  ccatpfx  14231  pfxccat1  14232  swrdswrd  14235  cshf1  14340  crim  14643  absmax  14858  ello12r  15043  elo12r  15054  climshftlem  15100  2sumeq2dv  15234  hash2iun  15350  expcnv  15391  2cprodeq2dv  15450  rpnnen2lem7  15744  dvdsval3  15782  dvdsnegb  15798  muldvds1  15805  muldvds2  15806  dvdscmul  15807  dvdsmulc  15808  dvdsmulcr  15810  dvds2ln  15813  divalgb  15928  ndvdssub  15933  gcddiv  16074  lcmfval  16141  lcmfcl  16148  dvdslcmf  16151  rpexp1i  16243  phiprmpw  16292  hashgcdeq  16305  pythagtriplem1  16332  pockthg  16422  infpnlem1  16426  4sqlem3  16466  0ramcl  16539  firest  16891  imasaddfnlem  16987  imasleval  17000  mrerintcl  17054  iscatd  17130  fullestrcsetc  17612  fullsetcestrc  17627  clatleglb  17978  mreclatBAD  18023  pslem  18032  mndind  18208  grplmulf1o  18391  grplactcnv  18420  mulgnn0subcl  18459  mulgsubcl  18460  mulgdir  18477  issubg2  18512  issubgrpd2  18513  nmzsubg  18535  eqgen  18551  cycsubm  18563  cycsubgcl  18567  cycsubgss  18568  ghmmulg  18588  conjghm  18607  symgpssefmnd  18742  gsmsymgreqlem2  18777  symgfixfo  18785  odeq  18896  odval2  18897  odf1  18907  dfod2  18909  gexdvds  18927  gexdvds2  18928  gexcl2  18932  gexdvds3  18933  sylow2blem2  18964  efgsp1  19081  efgrelexlemb  19094  mulgmhm  19167  mulgghm  19168  iscyggen2  19219  iscyg3  19224  ablsimpgfindlem1  19448  srglmhm  19504  srgrmhm  19505  ringlghm  19576  ringrghm  19577  gsumdixp  19581  dvdsrcl2  19622  crngunit  19634  kerf1ghm  19717  subrgugrp  19773  cntzsubr  19787  sdrgacs  19799  lmodvsdir  19877  lmodvsass  19878  lmodvsghm  19914  lsssubg  19948  lss1d  19954  islbs2  20145  lidlsubg  20207  lidlsubcl  20208  quscrng  20232  lpigen  20248  xrsdsreval  20362  expghm  20416  mulgghm2  20417  ip0r  20553  obs2ss  20645  islindf3  20742  scmatscm  21364  scmataddcl  21367  scmatsubcl  21368  scmatfo  21381  matunit  21529  cpmatelimp  21563  cpmatelimp2  21565  cpmatinvcl  21568  cpmatmcl  21570  mat2pmatf  21579  m2cpmf  21593  cpm2mf  21603  m2cpmfo  21607  m2cpminv  21611  decpmataa0  21619  pm2mpf  21649  pm2mpf1  21650  idpm2idmp  21652  pm2mpfo  21665  elcls2  21925  opnnei  21971  innei  21976  iscnp4  22114  cnpnei  22115  iscncl  22120  cnnei  22133  cnconst  22135  ordthauslem  22234  bwth  22261  1stccnp  22313  llyrest  22336  nllyrest  22337  kgenss  22394  xkoccn  22470  kqsat  22582  kqt0lem  22587  isr0  22588  fbssfi  22688  isfild  22709  filconn  22734  trfilss  22740  fgtr  22741  ufileu  22770  ufilen  22781  fmfnfmlem4  22808  fmfnfm  22809  hausflimi  22831  cnpflf2  22851  cnpflf  22852  cnpfcf  22892  cnextcn  22918  tsmsxplem1  23004  tsmsxp  23006  ustuqtop0  23092  ismeti  23177  isxmet2d  23179  elbl2ps  23241  elbl2  23242  xblpnfps  23247  xblpnf  23248  xbln0  23266  blin  23273  blssexps  23278  blssex  23279  blcls  23358  blsscls  23359  metrest  23376  metustbl  23418  psmetutop  23419  nmf2  23445  ngpi  23480  tngngp3  23508  nmdvr  23522  nmoi  23580  nmoix  23581  nmoleub  23583  nghmcn  23597  iccntr  23672  metdsle  23703  icoopnst  23790  iocopnst  23791  icccvx  23801  pi1xfr  23906  isclmi0  23949  iscvsi  23980  cphipval  24094  lmmbr  24109  lmmbr2  24110  iscfil3  24124  iscau2  24128  cfilres  24147  bcthlem1  24175  bcthlem4  24178  bcthlem5  24179  rrxmet  24259  ioombl  24416  iccvolcl  24418  ioovolcl  24421  mbfi1fseqlem3  24569  mbfi1fseqlem4  24570  mbfi1fseqlem5  24571  ig1pcl  25027  ig1prsp  25029  aannenlem1  25175  taylplem1  25209  dvtaylp  25216  relogeftb  25427  logdivlt  25463  cxpexp  25510  rpcxpcl  25518  isppw2  25951  vmappw  25952  lgslem4  26135  lgscllem  26139  lgsneg1  26157  lgsne0  26170  brbtwn2  26950  ax5seglem1  26973  ax5seglem2  26974  axcontlem4  27012  ewlkprop  27645  uspgr2wlkeq  27687  uhgrwkspthlem2  27795  clwlkclwwlkfo  28046  eupth2lem3lem7  28271  frgr3vlem2  28311  3cyclfrgrrn1  28322  4cycl2vnunb  28327  frgrncvvdeqlem8  28343  grpoidinvlem3  28541  isvciOLD  28615  nmcvcn  28730  ipval2lem2  28739  sspimsval  28773  isblo2  28818  nmoo0  28826  blocni  28840  isph  28857  hvadd4  29071  hiassdi  29126  ocsh  29318  chj4  29570  spansncol  29603  pjjsi  29735  hoscl  29780  hodcl  29782  hoadd4  29819  homco1  29836  homulass  29837  hoadddi  29838  hoadddir  29839  unoplin  29955  adjvalval  29972  hmoplin  29977  bralnfn  29983  brafnmul  29986  lnopmi  30035  lnopcoi  30038  hmops  30055  hmopm  30056  nmophmi  30066  lnfncnbd  30092  cnlnadjlem2  30103  adjlnop  30121  adjmul  30127  adjadd  30128  branmfn  30140  kbass5  30155  kbass6  30156  leop2  30159  leopadd  30167  leopmuli  30168  pjimai  30211  atcvatlem  30420  chirredlem2  30426  mdsymlem3  30440  mdsymlem5  30442  sumdmdii  30450  sumdmdlem  30453  cdj3lem2a  30471  cdj3lem2b  30472  cdj3lem3a  30474  cdj3i  30476  xreceu  30870  cshwrnid  30907  toslublem  30923  tosglblem  30925  lmodvslmhm  30983  ogrpaddltbi  31017  archiabllem1b  31119  archiabllem2c  31122  archiabl  31125  slmdvsdir  31142  slmdvsass  31143  grplsm0l  31259  zarcls1  31487  pstmxmet  31515  ordtconnlem1  31542  hasheuni  31719  omsf  31929  ballotlemirc  32164  signswmnd  32202  bnj1204  32659  fineqvac  32733  fisshasheq  32740  revpfxsfxrev  32744  txpconn  32861  cvmscld  32902  satfbrsuc  32995  satfrnmapom  32999  satfun  33040  elmpps  33202  dfrdg2  33441  wsuclem  33499  nosepdm  33573  ssltdisj  33701  segconeu  33999  linecom  34138  linethru  34141  lineintmo  34145  fnemeet2  34242  fnejoin2  34244  fvineqsneq  35269  lindsadd  35456  lindsdom  35457  lindsenlbs  35458  matunitlindflem1  35459  matunitlindflem2  35460  heicant  35498  mblfinlem1  35500  mblfinlem3  35502  ismblfin  35504  cnambfre  35511  itg2addnclem2  35515  ftc1anclem1  35536  ftc1anclem5  35540  ftc1anclem6  35541  ftc2nc  35545  areacirclem2  35552  areacirclem4  35554  areacirclem5  35555  areacirc  35556  fzmul  35585  subspopn  35596  isbndx  35626  isbnd2  35627  isbnd3  35628  ssbnd  35632  prdstotbnd  35638  heibor1  35654  rrnmet  35673  rngonegmn1l  35785  rngohomco  35818  rngoisocnv  35825  rngoisoco  35826  crngohomfo  35850  isidlc  35859  rngoidl  35868  prnc  35911  ispridlc  35914  cvrval2  36974  glbconxN  37078  hlrelat5N  37101  cvratlem  37121  cvrat2  37129  athgt  37156  3dim2  37168  llnn0  37216  lplnn0N  37247  lvoln0N  37291  snatpsubN  37450  paddasslem18  37537  pmod1i  37548  lhpexle2  37710  lhpexle3lem  37711  lhpexle3  37712  ldilcnv  37815  trlcnv  37865  trlnidatb  37877  cdleme32snaw  38135  cdleme32fvaw  38139  cdleme42ke  38185  cdlemeg46gf  38233  cdleme50trn12  38252  cdlemg1cex  38288  cdlemb3  38306  tgrpgrplem  38449  tgrpabl  38451  tendoplcl2  38478  tendo0pl  38491  tendoicl  38496  tendoipl  38497  cdlemkid3N  38633  tendoex  38675  erngdvlem4  38691  erngdvlem4-rN  38699  dib1dim  38865  dib1dim2  38868  dihglbcpreN  39000  dihmeetALTN  39027  dih1dimatlem  39029  dihatlat  39034  fzindd  39667  lcmineqlem1  39720  lcmineqlem3  39722  aks4d1p1  39766  sticksstones1  39771  sticksstones2  39772  sticksstones3  39773  sticksstones8  39778  sticksstones10  39780  sticksstones11  39781  sticksstones12a  39782  sticksstones12  39783  metakunt29  39816  metakunt30  39817  metakunt31  39818  factwoffsmonot  39826  oddcomabszz  40410  acongtr  40444  rpnnen3lem  40497  islssfg  40539  lmhmfgsplit  40555  unxpwdom3  40564  hbtlem7  40594  iocmbl  40688  ss2iundf  40885  ismnu  41493  grumnudlem  41517  ismnushort  41533  nzss  41549  dvconstbi  41566  bccbc  41577  uzmptshftfval  41578  iccdifprioo  42670  climisp  42905  limsupresxr  42925  liminfresxr  42926  dvnmul  43102  volico  43142  volioore  43149  fourierdlem74  43339  fourierdlem75  43340  sge0iunmptlemfi  43569  sge0iunmptlemre  43571  sge0iunmpt  43574  sge0xp  43585  hspmbllem2  43783  smflimlem3  43923  smfsupmpt  43963  smfinflem  43965  smfinfmpt  43967  smflimsupmpt  43977  smfliminfmpt  43980  funressnbrafv2  44351  uniimaelsetpreimafv  44464  imasetpreimafvbijlemfv1  44471  imasetpreimafvbijlemfo  44473  sprsymrelfo  44565  nnsum4primesodd  44864  nnsum4primesoddALTV  44865  nn0mnd  44989  rnghmsubcsetclem2  45150  rhmsubcsetclem2  45196  rhmsubcrngclem2  45202  lcoss  45393  snlindsntorlem  45427  mreclat  45899  aacllem  46119