Theorem 3expa 1118

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1087

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 1089

This theorem is referenced by:  3exp  1119  ad4ant123  1172  ad4ant124  1173  ad4ant134  1174  ad4ant234  1175  ad5ant123  1364  3anidm23  1421  mp3an2  1449  mpd3an3  1462  rgen3  3201  vtocl3  3549  spc3egv  3590  moi2  3708  sbc3ie  3859  2if2  4577  preq12bg  4847  ralxfrd2  5403  reuhypd  5410  otsndisj  5512  funcnvqp  6601  fvtp1g  7183  fntpb  7195  f1imass  7247  weisoeq  7336  f1ofveu  7387  f1ocnvfv3  7388  funeldmdif  8016  curry1f  8074  curry2f  8076  funsssuppss  8157  frrlem13  8265  tfrlem11  8370  oalimcl  8543  oeordsuc  8577  oelim2  8578  nneob  8638  nadd4  8680  mapxpen  9126  findcard  9146  enfii  9172  domtrfil  9178  domnsymfi  9186  phplem2  9191  php  9193  wemaplem3  9525  en2eqpr  9984  infxpabs  10189  infxp  10192  cfflb  10236  cfsmolem  10247  isf32lem12  10341  fin1a2lem9  10385  fin1a2s  10391  axcc3  10415  axdc3lem4  10430  zornn0g  10482  pwfseqlem4  10639  tskwun  10761  tskint  10762  tskxp  10764  tskmap  10765  gruf  10788  grutsk1  10798  addcanpi  10876  ltapi  10880  mul4  11364  add4  11416  2addsub  11456  addsubeq4  11457  muladd  11628  ltleadd  11679  receu  11841  p1le  12041  lbinf  12149  zdiv  12614  fzind  12642  fnn0ind  12643  fzindd  12646  uzss  12827  zbtwnre  12912  qmulcl  12933  qreccl  12935  xrlttr  13101  xaddass  13210  xmulasslem3  13247  xadddilem  13255  xrsupsslem  13268  xrinfmsslem  13269  supxrunb1  13280  ioo0  13331  ico0  13352  ioc0  13353  icc0  13354  iooshf  13385  prunioo  13440  ioojoin  13442  elfz5  13475  elfz0fzfz0  13588  elfzonelfzo  13716  fzind2  13732  mulexpz  14050  expsub  14058  digit1  14182  facndiv  14230  faclbnd4lem4  14238  faclbnd4  14239  faclbnd5  14240  bccmpl  14251  bcval5  14260  bcpasc  14263  hashunx  14328  hashunsnggt  14336  hashdmpropge2  14426  ccatrn  14521  swrdspsleq  14597  swrdccat2  14601  ccatpfx  14633  pfxccat1  14634  swrdswrd  14637  cshf1  14742  crim  15044  absmax  15258  ello12r  15443  elo12r  15454  climshftlem  15500  2sumeq2dv  15633  hash2iun  15751  expcnv  15792  2cprodeq2dv  15851  rpnnen2lem7  16145  dvdsval3  16183  dvdsnegb  16199  muldvds1  16206  muldvds2  16207  dvdscmul  16208  dvdsmulc  16209  dvdsmulcr  16211  dvds2ln  16214  divalgb  16329  ndvdssub  16334  gcddiv  16475  lcmfval  16540  lcmfcl  16547  dvdslcmf  16550  rpexp1i  16642  phiprmpw  16691  hashgcdeq  16704  pythagtriplem1  16731  pockthg  16821  infpnlem1  16825  4sqlem3  16865  0ramcl  16938  firest  17360  imasaddfnlem  17456  imasleval  17469  mrerintcl  17523  iscatd  17599  fullestrcsetc  18085  fullsetcestrc  18100  clatleglb  18453  mreclatBAD  18498  pslem  18507  mndind  18684  grplmulf1o  18871  grplactcnv  18900  mulgnn0subcl  18939  mulgsubcl  18940  mulgdir  18958  issubg2  18993  issubgrpd2  18994  nmzsubg  19017  eqgen  19033  cycsubm  19045  cycsubgcl  19049  cycsubgss  19050  ghmmulg  19070  conjghm  19089  symgpssefmnd  19227  gsmsymgreqlem2  19263  symgfixfo  19271  odeq  19382  odval2  19383  odf1  19394  dfod2  19396  gexdvds  19416  gexdvds2  19417  gexcl2  19421  gexdvds3  19422  sylow2blem2  19453  efgsp1  19569  efgrelexlemb  19582  mulgmhm  19656  mulgghm  19657  iscyggen2  19708  iscyg3  19713  ablsimpgfindlem1  19936  srglmhm  20002  srgrmhm  20003  ringlghm  20081  ringrghm  20082  gsumdixp  20086  dvdsrcl2  20132  crngunit  20144  kerf1ghm  20232  subrgugrp  20331  cntzsubr  20347  sdrgacs  20366  lmodvsdir  20445  lmodvsass  20446  lmodvsghm  20482  lsssubg  20517  lss1d  20523  islbs2  20716  lidlsubg  20786  lidlsubcl  20787  quscrng  20814  lpigen  20830  xrsdsreval  20924  expghm  20978  mulgghm2  20979  ip0r  21123  obs2ss  21217  islindf3  21314  scmatscm  21944  scmataddcl  21947  scmatsubcl  21948  scmatfo  21961  matunit  22109  cpmatelimp  22143  cpmatelimp2  22145  cpmatinvcl  22148  cpmatmcl  22150  mat2pmatf  22159  m2cpmf  22173  cpm2mf  22183  m2cpmfo  22187  m2cpminv  22191  decpmataa0  22199  pm2mpf  22229  pm2mpf1  22230  idpm2idmp  22232  pm2mpfo  22245  elcls2  22507  opnnei  22553  innei  22558  iscnp4  22696  cnpnei  22697  iscncl  22702  cnnei  22715  cnconst  22717  ordthauslem  22816  bwth  22843  1stccnp  22895  llyrest  22918  nllyrest  22919  kgenss  22976  xkoccn  23052  kqsat  23164  kqt0lem  23169  isr0  23170  fbssfi  23270  isfild  23291  filconn  23316  trfilss  23322  fgtr  23323  ufileu  23352  ufilen  23363  fmfnfmlem4  23390  fmfnfm  23391  hausflimi  23413  cnpflf2  23433  cnpflf  23434  cnpfcf  23474  cnextcn  23500  tsmsxplem1  23586  tsmsxp  23588  ustuqtop0  23674  ismeti  23760  isxmet2d  23762  elbl2ps  23824  elbl2  23825  xblpnfps  23830  xblpnf  23831  xbln0  23849  blin  23856  blssexps  23861  blssex  23862  blcls  23944  blsscls  23945  metrest  23962  metustbl  24004  psmetutop  24005  nmf2  24031  ngpi  24066  tngngp3  24102  nmdvr  24116  nmoi  24174  nmoix  24175  nmoleub  24177  nghmcn  24191  iccntr  24266  metdsle  24297  icoopnst  24384  iocopnst  24385  icccvx  24395  pi1xfr  24500  isclmi0  24543  iscvsi  24574  cphipval  24689  lmmbr  24704  lmmbr2  24705  iscfil3  24719  iscau2  24723  cfilres  24742  bcthlem1  24770  bcthlem4  24773  bcthlem5  24774  rrxmet  24854  ioombl  25011  iccvolcl  25013  ioovolcl  25016  mbfi1fseqlem3  25164  mbfi1fseqlem4  25165  mbfi1fseqlem5  25166  ig1pcl  25622  ig1prsp  25624  aannenlem1  25770  taylplem1  25804  dvtaylp  25811  relogeftb  26022  logdivlt  26058  cxpexp  26105  rpcxpcl  26113  isppw2  26546  vmappw  26547  lgslem4  26730  lgscllem  26734  lgsneg1  26752  lgsne0  26765  nosepdm  27114  ssltdisj  27248  mulscutlem  27500  brbtwn2  28028  ax5seglem1  28051  ax5seglem2  28052  axcontlem4  28090  ewlkprop  28725  uspgr2wlkeq  28768  uhgrwkspthlem2  28876  clwlkclwwlkfo  29127  eupth2lem3lem7  29352  frgr3vlem2  29392  3cyclfrgrrn1  29403  4cycl2vnunb  29408  frgrncvvdeqlem8  29424  grpoidinvlem3  29622  isvciOLD  29696  nmcvcn  29811  ipval2lem2  29820  sspimsval  29854  isblo2  29899  nmoo0  29907  blocni  29921  isph  29938  hvadd4  30152  hiassdi  30207  ocsh  30399  chj4  30651  spansncol  30684  pjjsi  30816  hoscl  30861  hodcl  30863  hoadd4  30900  homco1  30917  homulass  30918  hoadddi  30919  hoadddir  30920  unoplin  31036  adjvalval  31053  hmoplin  31058  bralnfn  31064  brafnmul  31067  lnopmi  31116  lnopcoi  31119  hmops  31136  hmopm  31137  nmophmi  31147  lnfncnbd  31173  cnlnadjlem2  31184  adjlnop  31202  adjmul  31208  adjadd  31209  branmfn  31221  kbass5  31236  kbass6  31237  leop2  31240  leopadd  31248  leopmuli  31249  pjimai  31292  atcvatlem  31501  chirredlem2  31507  mdsymlem3  31521  mdsymlem5  31523  sumdmdii  31531  sumdmdlem  31534  cdj3lem2a  31552  cdj3lem2b  31553  cdj3lem3a  31555  cdj3i  31557  nn0difffzod  31887  xreceu  31959  cshwrnid  31996  toslublem  32013  tosglblem  32015  lmodvslmhm  32073  ogrpaddltbi  32107  archiabllem1b  32209  archiabllem2c  32212  archiabl  32215  slmdvsdir  32232  slmdvsass  32233  grplsm0l  32371  zarcls1  32680  pstmxmet  32708  ordtconnlem1  32735  hasheuni  32914  omsf  33126  ballotlemirc  33361  signswmnd  33399  bnj1204  33854  fineqvac  33928  fisshasheq  33935  revpfxsfxrev  33937  txpconn  34054  cvmscld  34095  satfbrsuc  34188  satfrnmapom  34192  satfun  34233  elmpps  34395  dfrdg2  34597  wsuclem  34627  segconeu  34813  linecom  34952  linethru  34955  lineintmo  34959  fnemeet2  35056  fnejoin2  35058  fvineqsneq  36097  lindsadd  36285  lindsdom  36286  lindsenlbs  36287  matunitlindflem1  36288  matunitlindflem2  36289  heicant  36327  mblfinlem1  36329  mblfinlem3  36331  ismblfin  36333  cnambfre  36340  itg2addnclem2  36344  ftc1anclem1  36365  ftc1anclem5  36369  ftc1anclem6  36370  ftc2nc  36374  areacirclem2  36381  areacirclem4  36383  areacirclem5  36384  areacirc  36385  fzmul  36414  subspopn  36425  isbndx  36455  isbnd2  36456  isbnd3  36457  ssbnd  36461  prdstotbnd  36467  heibor1  36483  rrnmet  36502  rngonegmn1l  36614  rngohomco  36647  rngoisocnv  36654  rngoisoco  36655  crngohomfo  36679  isidlc  36688  rngoidl  36697  prnc  36740  ispridlc  36743  cvrval2  37949  glbconxN  38054  hlrelat5N  38077  cvratlem  38097  cvrat2  38105  athgt  38132  3dim2  38144  llnn0  38192  lplnn0N  38223  lvoln0N  38267  snatpsubN  38426  paddasslem18  38513  pmod1i  38524  lhpexle2  38686  lhpexle3lem  38687  lhpexle3  38688  ldilcnv  38791  trlcnv  38841  trlnidatb  38853  cdleme32snaw  39111  cdleme32fvaw  39115  cdleme42ke  39161  cdlemeg46gf  39209  cdleme50trn12  39228  cdlemg1cex  39264  cdlemb3  39282  tgrpgrplem  39425  tgrpabl  39427  tendoplcl2  39454  tendo0pl  39467  tendoicl  39472  tendoipl  39473  cdlemkid3N  39609  tendoex  39651  erngdvlem4  39667  erngdvlem4-rN  39675  dib1dim  39841  dib1dim2  39844  dihglbcpreN  39976  dihmeetALTN  40003  dih1dimatlem  40005  dihatlat  40010  lcmineqlem1  40699  lcmineqlem3  40701  aks4d1p1  40746  aks4d1p7d1  40752  aks4d1p8  40757  sticksstones1  40767  sticksstones2  40768  sticksstones3  40769  sticksstones8  40774  sticksstones10  40776  sticksstones11  40777  sticksstones12a  40778  sticksstones12  40779  sticksstones17  40784  sticksstones19  40786  metakunt29  40818  metakunt30  40819  metakunt31  40820  factwoffsmonot  40828  oddcomabszz  41454  acongtr  41488  rpnnen3lem  41541  islssfg  41583  lmhmfgsplit  41599  unxpwdom3  41608  hbtlem7  41638  iocmbl  41733  ss2iundf  42181  ismnu  42791  grumnudlem  42815  ismnushort  42831  nzss  42847  dvconstbi  42864  bccbc  42875  uzmptshftfval  42876  iccdifprioo  44002  climisp  44235  limsupresxr  44255  liminfresxr  44256  dvnmul  44432  volico  44472  volioore  44479  fourierdlem74  44669  fourierdlem75  44670  sge0iunmptlemfi  44902  sge0iunmptlemre  44904  sge0iunmpt  44907  sge0xp  44918  hspmbllem2  45116  smflimlem3  45262  smfsupmpt  45304  smfinflem  45306  smfinfmpt  45308  smflimsupmpt  45318  smfliminfmpt  45321  funressnbrafv2  45724  uniimaelsetpreimafv  45836  imasetpreimafvbijlemfv1  45843  imasetpreimafvbijlemfo  45845  sprsymrelfo  45937  nnsum4primesodd  46236  nnsum4primesoddALTV  46237  nn0mnd  46361  rnghmsubcsetclem2  46522  rhmsubcsetclem2  46568  rhmsubcrngclem2  46574  lcoss  46765  snlindsntorlem  46799  mreclat  47270  aacllem  47496