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  1447  mpd3an3  1460  rgen3  3127  vtocl3  3491  spc3egv  3532  moi2  3646  sbc3ie  3798  2if2  4511  preq12bg  4781  ralxfrd2  5330  reuhypd  5337  otsndisj  5427  funcnvqp  6482  fvtp1g  7055  fntpb  7067  f1imass  7118  weisoeq  7206  f1ofveu  7250  f1ocnvfv3  7251  funeldmdif  7862  curry1f  7917  curry2f  7919  funsssuppss  7977  frrlem13  8085  tfrlem11  8190  oalimcl  8353  oeordsuc  8387  oelim2  8388  nneob  8446  mapxpen  8879  findcard  8908  enfii  8932  wemaplem3  9237  en2eqpr  9694  infxpabs  9899  infxp  9902  cfflb  9946  cfsmolem  9957  isf32lem12  10051  fin1a2lem9  10095  fin1a2s  10101  axcc3  10125  axdc3lem4  10140  zornn0g  10192  pwfseqlem4  10349  tskwun  10471  tskint  10472  tskxp  10474  tskmap  10475  gruf  10498  grutsk1  10508  addcanpi  10586  ltapi  10590  mul4  11073  add4  11125  2addsub  11165  addsubeq4  11166  muladd  11337  ltleadd  11388  receu  11550  p1le  11750  lbinf  11858  zdiv  12320  fzind  12348  fnn0ind  12349  uzss  12534  zbtwnre  12615  qmulcl  12636  qreccl  12638  xrlttr  12803  xaddass  12912  xmulasslem3  12949  xadddilem  12957  xrsupsslem  12970  xrinfmsslem  12971  supxrunb1  12982  ioo0  13033  ico0  13054  ioc0  13055  icc0  13056  iooshf  13087  prunioo  13142  ioojoin  13144  elfz5  13177  elfz0fzfz0  13290  elfzonelfzo  13417  fzind2  13433  mulexpz  13751  expsub  13759  digit1  13880  facndiv  13930  faclbnd4lem4  13938  faclbnd4  13939  faclbnd5  13940  bccmpl  13951  bcval5  13960  bcpasc  13963  hashunx  14029  hashunsnggt  14037  hashdmpropge2  14125  ccatrn  14222  swrdspsleq  14306  swrdccat2  14310  ccatpfx  14342  pfxccat1  14343  swrdswrd  14346  cshf1  14451  crim  14754  absmax  14969  ello12r  15154  elo12r  15165  climshftlem  15211  2sumeq2dv  15345  hash2iun  15463  expcnv  15504  2cprodeq2dv  15563  rpnnen2lem7  15857  dvdsval3  15895  dvdsnegb  15911  muldvds1  15918  muldvds2  15919  dvdscmul  15920  dvdsmulc  15921  dvdsmulcr  15923  dvds2ln  15926  divalgb  16041  ndvdssub  16046  gcddiv  16187  lcmfval  16254  lcmfcl  16261  dvdslcmf  16264  rpexp1i  16356  phiprmpw  16405  hashgcdeq  16418  pythagtriplem1  16445  pockthg  16535  infpnlem1  16539  4sqlem3  16579  0ramcl  16652  firest  17060  imasaddfnlem  17156  imasleval  17169  mrerintcl  17223  iscatd  17299  fullestrcsetc  17784  fullsetcestrc  17799  clatleglb  18151  mreclatBAD  18196  pslem  18205  mndind  18381  grplmulf1o  18564  grplactcnv  18593  mulgnn0subcl  18632  mulgsubcl  18633  mulgdir  18650  issubg2  18685  issubgrpd2  18686  nmzsubg  18708  eqgen  18724  cycsubm  18736  cycsubgcl  18740  cycsubgss  18741  ghmmulg  18761  conjghm  18780  symgpssefmnd  18918  gsmsymgreqlem2  18954  symgfixfo  18962  odeq  19073  odval2  19074  odf1  19084  dfod2  19086  gexdvds  19104  gexdvds2  19105  gexcl2  19109  gexdvds3  19110  sylow2blem2  19141  efgsp1  19258  efgrelexlemb  19271  mulgmhm  19344  mulgghm  19345  iscyggen2  19396  iscyg3  19401  ablsimpgfindlem1  19625  srglmhm  19686  srgrmhm  19687  ringlghm  19758  ringrghm  19759  gsumdixp  19763  dvdsrcl2  19807  crngunit  19819  kerf1ghm  19902  subrgugrp  19958  cntzsubr  19972  sdrgacs  19984  lmodvsdir  20062  lmodvsass  20063  lmodvsghm  20099  lsssubg  20134  lss1d  20140  islbs2  20331  lidlsubg  20399  lidlsubcl  20400  quscrng  20424  lpigen  20440  xrsdsreval  20555  expghm  20609  mulgghm2  20610  ip0r  20754  obs2ss  20846  islindf3  20943  scmatscm  21570  scmataddcl  21573  scmatsubcl  21574  scmatfo  21587  matunit  21735  cpmatelimp  21769  cpmatelimp2  21771  cpmatinvcl  21774  cpmatmcl  21776  mat2pmatf  21785  m2cpmf  21799  cpm2mf  21809  m2cpmfo  21813  m2cpminv  21817  decpmataa0  21825  pm2mpf  21855  pm2mpf1  21856  idpm2idmp  21858  pm2mpfo  21871  elcls2  22133  opnnei  22179  innei  22184  iscnp4  22322  cnpnei  22323  iscncl  22328  cnnei  22341  cnconst  22343  ordthauslem  22442  bwth  22469  1stccnp  22521  llyrest  22544  nllyrest  22545  kgenss  22602  xkoccn  22678  kqsat  22790  kqt0lem  22795  isr0  22796  fbssfi  22896  isfild  22917  filconn  22942  trfilss  22948  fgtr  22949  ufileu  22978  ufilen  22989  fmfnfmlem4  23016  fmfnfm  23017  hausflimi  23039  cnpflf2  23059  cnpflf  23060  cnpfcf  23100  cnextcn  23126  tsmsxplem1  23212  tsmsxp  23214  ustuqtop0  23300  ismeti  23386  isxmet2d  23388  elbl2ps  23450  elbl2  23451  xblpnfps  23456  xblpnf  23457  xbln0  23475  blin  23482  blssexps  23487  blssex  23488  blcls  23568  blsscls  23569  metrest  23586  metustbl  23628  psmetutop  23629  nmf2  23655  ngpi  23690  tngngp3  23726  nmdvr  23740  nmoi  23798  nmoix  23799  nmoleub  23801  nghmcn  23815  iccntr  23890  metdsle  23921  icoopnst  24008  iocopnst  24009  icccvx  24019  pi1xfr  24124  isclmi0  24167  iscvsi  24198  cphipval  24312  lmmbr  24327  lmmbr2  24328  iscfil3  24342  iscau2  24346  cfilres  24365  bcthlem1  24393  bcthlem4  24396  bcthlem5  24397  rrxmet  24477  ioombl  24634  iccvolcl  24636  ioovolcl  24639  mbfi1fseqlem3  24787  mbfi1fseqlem4  24788  mbfi1fseqlem5  24789  ig1pcl  25245  ig1prsp  25247  aannenlem1  25393  taylplem1  25427  dvtaylp  25434  relogeftb  25645  logdivlt  25681  cxpexp  25728  rpcxpcl  25736  isppw2  26169  vmappw  26170  lgslem4  26353  lgscllem  26357  lgsneg1  26375  lgsne0  26388  brbtwn2  27176  ax5seglem1  27199  ax5seglem2  27200  axcontlem4  27238  ewlkprop  27873  uspgr2wlkeq  27915  uhgrwkspthlem2  28023  clwlkclwwlkfo  28274  eupth2lem3lem7  28499  frgr3vlem2  28539  3cyclfrgrrn1  28550  4cycl2vnunb  28555  frgrncvvdeqlem8  28571  grpoidinvlem3  28769  isvciOLD  28843  nmcvcn  28958  ipval2lem2  28967  sspimsval  29001  isblo2  29046  nmoo0  29054  blocni  29068  isph  29085  hvadd4  29299  hiassdi  29354  ocsh  29546  chj4  29798  spansncol  29831  pjjsi  29963  hoscl  30008  hodcl  30010  hoadd4  30047  homco1  30064  homulass  30065  hoadddi  30066  hoadddir  30067  unoplin  30183  adjvalval  30200  hmoplin  30205  bralnfn  30211  brafnmul  30214  lnopmi  30263  lnopcoi  30266  hmops  30283  hmopm  30284  nmophmi  30294  lnfncnbd  30320  cnlnadjlem2  30331  adjlnop  30349  adjmul  30355  adjadd  30356  branmfn  30368  kbass5  30383  kbass6  30384  leop2  30387  leopadd  30395  leopmuli  30396  pjimai  30439  atcvatlem  30648  chirredlem2  30654  mdsymlem3  30668  mdsymlem5  30670  sumdmdii  30678  sumdmdlem  30681  cdj3lem2a  30699  cdj3lem2b  30700  cdj3lem3a  30702  cdj3i  30704  xreceu  31098  cshwrnid  31135  toslublem  31152  tosglblem  31154  lmodvslmhm  31212  ogrpaddltbi  31246  archiabllem1b  31348  archiabllem2c  31351  archiabl  31354  slmdvsdir  31371  slmdvsass  31372  grplsm0l  31493  zarcls1  31721  pstmxmet  31749  ordtconnlem1  31776  hasheuni  31953  omsf  32163  ballotlemirc  32398  signswmnd  32436  bnj1204  32892  fineqvac  32966  fisshasheq  32973  revpfxsfxrev  32977  txpconn  33094  cvmscld  33135  satfbrsuc  33228  satfrnmapom  33232  satfun  33273  elmpps  33435  dfrdg2  33677  wsuclem  33746  nosepdm  33814  ssltdisj  33942  segconeu  34240  linecom  34379  linethru  34382  lineintmo  34386  fnemeet2  34483  fnejoin2  34485  fvineqsneq  35510  lindsadd  35697  lindsdom  35698  lindsenlbs  35699  matunitlindflem1  35700  matunitlindflem2  35701  heicant  35739  mblfinlem1  35741  mblfinlem3  35743  ismblfin  35745  cnambfre  35752  itg2addnclem2  35756  ftc1anclem1  35777  ftc1anclem5  35781  ftc1anclem6  35782  ftc2nc  35786  areacirclem2  35793  areacirclem4  35795  areacirclem5  35796  areacirc  35797  fzmul  35826  subspopn  35837  isbndx  35867  isbnd2  35868  isbnd3  35869  ssbnd  35873  prdstotbnd  35879  heibor1  35895  rrnmet  35914  rngonegmn1l  36026  rngohomco  36059  rngoisocnv  36066  rngoisoco  36067  crngohomfo  36091  isidlc  36100  rngoidl  36109  prnc  36152  ispridlc  36155  cvrval2  37215  glbconxN  37319  hlrelat5N  37342  cvratlem  37362  cvrat2  37370  athgt  37397  3dim2  37409  llnn0  37457  lplnn0N  37488  lvoln0N  37532  snatpsubN  37691  paddasslem18  37778  pmod1i  37789  lhpexle2  37951  lhpexle3lem  37952  lhpexle3  37953  ldilcnv  38056  trlcnv  38106  trlnidatb  38118  cdleme32snaw  38376  cdleme32fvaw  38380  cdleme42ke  38426  cdlemeg46gf  38474  cdleme50trn12  38493  cdlemg1cex  38529  cdlemb3  38547  tgrpgrplem  38690  tgrpabl  38692  tendoplcl2  38719  tendo0pl  38732  tendoicl  38737  tendoipl  38738  cdlemkid3N  38874  tendoex  38916  erngdvlem4  38932  erngdvlem4-rN  38940  dib1dim  39106  dib1dim2  39109  dihglbcpreN  39241  dihmeetALTN  39268  dih1dimatlem  39270  dihatlat  39275  fzindd  39912  lcmineqlem1  39965  lcmineqlem3  39967  aks4d1p1  40012  aks4d1p7d1  40018  aks4d1p8  40023  sticksstones1  40030  sticksstones2  40031  sticksstones3  40032  sticksstones8  40037  sticksstones10  40039  sticksstones11  40040  sticksstones12a  40041  sticksstones12  40042  sticksstones17  40047  sticksstones19  40049  metakunt29  40081  metakunt30  40082  metakunt31  40083  factwoffsmonot  40091  oddcomabszz  40682  acongtr  40716  rpnnen3lem  40769  islssfg  40811  lmhmfgsplit  40827  unxpwdom3  40836  hbtlem7  40866  iocmbl  40960  ss2iundf  41156  ismnu  41768  grumnudlem  41792  ismnushort  41808  nzss  41824  dvconstbi  41841  bccbc  41852  uzmptshftfval  41853  iccdifprioo  42944  climisp  43177  limsupresxr  43197  liminfresxr  43198  dvnmul  43374  volico  43414  volioore  43421  fourierdlem74  43611  fourierdlem75  43612  sge0iunmptlemfi  43841  sge0iunmptlemre  43843  sge0iunmpt  43846  sge0xp  43857  hspmbllem2  44055  smflimlem3  44195  smfsupmpt  44235  smfinflem  44237  smfinfmpt  44239  smflimsupmpt  44249  smfliminfmpt  44252  funressnbrafv2  44623  uniimaelsetpreimafv  44736  imasetpreimafvbijlemfv1  44743  imasetpreimafvbijlemfo  44745  sprsymrelfo  44837  nnsum4primesodd  45136  nnsum4primesoddALTV  45137  nn0mnd  45261  rnghmsubcsetclem2  45422  rhmsubcsetclem2  45468  rhmsubcrngclem2  45474  lcoss  45665  snlindsntorlem  45699  mreclat  46171  aacllem  46391