Theorem 3expa 1124

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

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

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 208  df-3an 1094

This theorem is referenced by:  3exp  1125  ad4ant123  1179  ad4ant124  1180  ad4ant134  1181  ad4ant234  1182  ad5ant123  1372  3anidm23  1429  mp3an2  1457  mpd3an3  1470  rgen3  3184  vtocl3  3511  spc3egv  3541  moi2  3657  sbc3ie  3800  2if2  4511  preq12bg  4785  ralxfrd2  5342  reuhypd  5349  otsndisj  5461  funcnvqp  6550  fvtp1g  7143  fntpb  7154  f1imass  7209  weisoeq  7300  f1ofveu  7351  f1ocnvfv3  7352  funeldmdif  7991  curry1f  8046  curry2f  8048  funsssuppss  8131  frrlem13  8239  tfrlem11  8318  oalimcl  8486  oeordsuc  8521  oelim2  8522  nneob  8583  nadd4  8625  mapxpen  9072  findcard  9089  enfii  9111  domtrfil  9117  domnsymfi  9125  phplem2  9130  php  9132  wemaplem3  9454  en2eqpr  9921  infxpabs  10125  infxp  10128  cfflb  10173  cfsmolem  10184  isf32lem12  10278  fin1a2lem9  10322  fin1a2s  10328  axcc3  10352  axdc3lem4  10367  zornn0g  10419  pwfseqlem4  10577  tskwun  10699  tskint  10700  tskxp  10702  tskmap  10703  gruf  10726  grutsk1  10736  addcanpi  10814  ltapi  10818  mul4  11306  add4  11359  2addsub  11399  addsubeq4  11400  muladd  11574  ltleadd  11625  receu  11787  p1le  11992  mulgt1  12009  lbinf  12101  zdiv  12591  fzind  12619  fnn0ind  12620  fzindd  12623  uzss  12803  zbtwnre  12888  qmulcl  12909  qreccl  12911  xrlttr  13083  xaddass  13193  xmulasslem3  13230  xadddilem  13238  xrsupsslem  13251  xrinfmsslem  13252  supxrunb1  13263  ioo0  13315  ico0  13336  ioc0  13337  icc0  13338  iooshf  13371  prunioo  13426  ioojoin  13428  elfz5  13462  elfz0fzfz0  13579  elfzonelfzo  13716  fzind2  13735  modaddb  13860  mulexpz  14056  expsub  14064  digit1  14191  facndiv  14242  faclbnd4lem4  14250  faclbnd4  14251  faclbnd5  14252  bccmpl  14263  bcval5  14272  bcpasc  14275  hashunx  14340  hashunsnggt  14348  hashdmpropge2  14437  ccatrn  14544  swrdspsleq  14620  swrdccat2  14624  ccatpfx  14655  pfxccat1  14656  swrdswrd  14659  cshf1  14764  crim  15069  absmax  15284  ello12r  15471  elo12r  15482  climshftlem  15528  2sumeq2dv  15659  hash2iun  15778  expcnv  15821  2cprodeq2dv  15882  rpnnen2lem7  16179  dvdsval3  16217  dvdsnegb  16234  muldvds1  16241  muldvds2  16242  dvdscmul  16243  dvdsmulc  16244  dvdsmulcr  16246  dvds2ln  16250  divalgb  16365  ndvdssub  16370  gcddiv  16512  lcmfval  16582  lcmfcl  16589  dvdslcmf  16592  rpexp1i  16685  phiprmpw  16738  hashgcdeq  16752  pythagtriplem1  16779  pockthg  16869  infpnlem1  16873  4sqlem3  16913  0ramcl  16986  firest  17387  imasaddfnlem  17484  imasleval  17497  mrerintcl  17551  iscatd  17631  fullestrcsetc  18109  fullsetcestrc  18124  clatleglb  18476  mreclatBAD  18521  pslem  18530  mndind  18788  grplmulf1o  18981  grplactcnv  19011  mulgnn0subcl  19055  mulgsubcl  19056  mulgdir  19074  issubg2  19109  issubgrpd2  19110  nmzsubg  19132  eqgen  19148  cycsubm  19169  cycsubgcl  19173  cycsubgss  19174  ghmmulg  19195  ghmf1  19213  kerf1ghm  19214  conjghm  19216  symgpssefmnd  19363  gsmsymgreqlem2  19398  symgfixfo  19406  odeq  19517  odval2  19518  odf1  19529  dfod2  19531  gexdvds  19551  gexdvds2  19552  gexcl2  19556  gexdvds3  19557  sylow2blem2  19588  efgsp1  19704  efgrelexlemb  19717  cmnbascntr  19772  mulgmhm  19794  mulgghm  19795  iscyggen2  19848  iscyg3  19853  ablsimpgfindlem1  20076  ogrpaddltbi  20106  srglmhm  20194  srgrmhm  20195  ringlghm  20285  ringrghm  20286  gsumdixp  20290  dvdsrcl2  20338  crngunit  20350  cntzsubrng  20540  subrgugrp  20564  cntzsubr  20579  rnghmsubcsetclem2  20605  rhmsubcsetclem2  20634  rhmsubcrngclem2  20640  sdrgacs  20774  lmodvsdir  20877  lmodvsass  20878  lmodvsghm  20914  lsssubg  20948  lss1d  20954  islbs2  21148  lidlsubg  21217  lidlsubcl  21218  rngqiprngimfo  21295  lpigen  21329  xrsdsreval  21388  expghm  21451  mulgghm2  21452  ip0r  21613  obs2ss  21705  islindf3  21802  scmatscm  22497  scmataddcl  22500  scmatsubcl  22501  scmatfo  22514  matunit  22662  cpmatelimp  22696  cpmatelimp2  22698  cpmatinvcl  22701  cpmatmcl  22703  mat2pmatf  22712  m2cpmf  22726  cpm2mf  22736  m2cpmfo  22740  m2cpminv  22744  decpmataa0  22752  pm2mpf  22782  pm2mpf1  22783  idpm2idmp  22785  pm2mpfo  22798  elcls2  23058  opnnei  23104  innei  23109  iscnp4  23247  cnpnei  23248  iscncl  23253  cnnei  23266  cnconst  23268  ordthauslem  23367  bwth  23394  1stccnp  23446  llyrest  23469  nllyrest  23470  kgenss  23527  xkoccn  23603  kqsat  23715  kqt0lem  23720  isr0  23721  fbssfi  23821  isfild  23842  filconn  23867  trfilss  23873  fgtr  23874  ufileu  23903  ufilen  23914  fmfnfmlem4  23941  fmfnfm  23942  hausflimi  23964  cnpflf2  23984  cnpflf  23985  cnpfcf  24025  cnextcn  24051  tsmsxplem1  24137  tsmsxp  24139  ustuqtop0  24224  ismeti  24309  isxmet2d  24311  elbl2ps  24373  elbl2  24374  xblpnfps  24379  xblpnf  24380  xbln0  24398  blin  24405  blssexps  24410  blssex  24411  blcls  24490  blsscls  24491  metrest  24508  metustbl  24550  psmetutop  24551  nmf2  24577  ngpi  24612  tngngp3  24640  nmdvr  24654  nmoi  24712  nmoix  24713  nmoleub  24715  nghmcn  24729  iccntr  24806  metdsle  24837  icoopnst  24925  iocopnst  24926  icccvx  24936  pi1xfr  25041  isclmi0  25084  iscvsi  25115  cphipval  25229  lmmbr  25244  lmmbr2  25245  iscfil3  25259  iscau2  25263  cfilres  25282  bcthlem1  25310  bcthlem4  25313  bcthlem5  25314  rrxmet  25394  ioombl  25551  iccvolcl  25553  ioovolcl  25556  mbfi1fseqlem3  25703  mbfi1fseqlem4  25704  mbfi1fseqlem5  25705  ig1pcl  26163  ig1prsp  26165  aannenlem1  26313  taylplem1  26347  dvtaylp  26354  relogeftb  26567  logdivlt  26604  cxpexp  26651  rpcxpcl  26659  isppw2  27097  vmappw  27098  lgslem4  27282  lgscllem  27286  lgsneg1  27304  lgsne0  27317  nosepdm  27667  sltsdisj  27814  mulcutlem  28142  ltonold  28272  zsoring  28420  bdayfinbndlem1  28478  z12bdaylem  28495  brbtwn2  28993  ax5seglem1  29016  ax5seglem2  29017  axcontlem4  29055  ewlkprop  29691  uspgr2wlkeq  29733  uhgrwkspthlem2  29841  clwlkclwwlkfo  30098  eupth2lem3lem7  30323  frgr3vlem2  30363  3cyclfrgrrn1  30374  4cycl2vnunb  30379  frgrncvvdeqlem8  30395  grpoidinvlem3  30596  isvciOLD  30670  nmcvcn  30785  ipval2lem2  30794  sspimsval  30828  isblo2  30873  nmoo0  30881  blocni  30895  isph  30912  hvadd4  31126  hiassdi  31181  ocsh  31373  chj4  31625  spansncol  31658  pjjsi  31790  hoscl  31835  hodcl  31837  hoadd4  31874  homco1  31891  homulass  31892  hoadddi  31893  hoadddir  31894  unoplin  32010  adjvalval  32027  hmoplin  32032  bralnfn  32038  brafnmul  32041  lnopmi  32090  lnopcoi  32093  hmops  32110  hmopm  32111  nmophmi  32121  lnfncnbd  32147  cnlnadjlem2  32158  adjlnop  32176  adjmul  32182  adjadd  32183  branmfn  32195  kbass5  32210  kbass6  32211  leop2  32214  leopadd  32222  leopmuli  32223  pjimai  32266  atcvatlem  32475  chirredlem2  32481  mdsymlem3  32495  mdsymlem5  32497  sumdmdii  32505  sumdmdlem  32508  cdj3lem2a  32526  cdj3lem2b  32527  cdj3lem3a  32529  cdj3i  32531  nn0difffzod  32897  xreceu  33001  cshwrnid  33041  toslublem  33052  tosglblem  33054  lmodvslmhm  33132  archiabllem1b  33274  archiabllem2c  33277  archiabl  33280  slmdvsdir  33298  slmdvsass  33299  grplsm0l  33487  pidlnzb  33506  rprmndvdsru  33621  mplvrpmmhm  33739  mplvrpmrhm  33740  zarcls1  34062  pstmxmet  34090  ordtconnlem1  34117  hasheuni  34278  omsf  34489  ballotlemirc  34725  signswmnd  34750  bnj1204  35203  fineqvac  35306  fisshasheq  35352  revpfxsfxrev  35353  txpconn  35469  cvmscld  35510  satfbrsuc  35603  satfrnmapom  35607  satfun  35648  elmpps  35810  dfrdg2  36030  wsuclem  36060  segconeu  36248  linecom  36387  linethru  36390  lineintmo  36394  fnemeet2  36604  fnejoin2  36606  fvineqsneq  37783  lindsadd  37989  lindsdom  37990  lindsenlbs  37991  matunitlindflem1  37992  matunitlindflem2  37993  heicant  38031  mblfinlem1  38033  mblfinlem3  38035  ismblfin  38037  cnambfre  38044  itg2addnclem2  38048  ftc1anclem1  38069  ftc1anclem5  38073  ftc1anclem6  38074  ftc2nc  38078  areacirclem2  38085  areacirclem4  38087  areacirclem5  38088  areacirc  38089  fzmul  38117  subspopn  38128  isbndx  38158  isbnd2  38159  isbnd3  38160  ssbnd  38164  prdstotbnd  38170  heibor1  38186  rrnmet  38205  rngonegmn1l  38317  rngohomco  38350  rngoisocnv  38357  rngoisoco  38358  crngohomfo  38382  isidlc  38391  rngoidl  38400  prnc  38443  ispridlc  38446  cvrval2  39775  glbconxN  39879  hlrelat5N  39902  cvratlem  39922  cvrat2  39930  athgt  39957  3dim2  39969  llnn0  40017  lplnn0N  40048  lvoln0N  40092  snatpsubN  40251  paddasslem18  40338  pmod1i  40349  lhpexle2  40511  lhpexle3lem  40512  lhpexle3  40513  ldilcnv  40616  trlcnv  40666  trlnidatb  40678  cdleme32snaw  40936  cdleme32fvaw  40940  cdleme42ke  40986  cdlemeg46gf  41034  cdleme50trn12  41053  cdlemg1cex  41089  cdlemb3  41107  tgrpgrplem  41250  tgrpabl  41252  tendoplcl2  41279  tendo0pl  41292  tendoicl  41297  tendoipl  41298  cdlemkid3N  41434  tendoex  41476  erngdvlem4  41492  erngdvlem4-rN  41500  dib1dim  41666  dib1dim2  41669  dihglbcpreN  41801  dihmeetALTN  41828  dih1dimatlem  41830  dihatlat  41835  lcmineqlem1  42523  lcmineqlem3  42525  aks4d1p1  42570  aks4d1p7d1  42576  aks4d1p8  42581  sticksstones1  42640  sticksstones2  42641  sticksstones3  42642  sticksstones8  42647  sticksstones10  42649  sticksstones11  42650  sticksstones12a  42651  sticksstones12  42652  sticksstones17  42657  sticksstones19  42659  oddcomabszz  43398  acongtr  43432  rpnnen3lem  43485  islssfg  43524  lmhmfgsplit  43540  unxpwdom3  43549  hbtlem7  43579  iocmbl  43667  ss2iundf  44112  ismnu  44714  grumnudlem  44738  ismnushort  44754  nzss  44770  dvconstbi  44787  bccbc  44798  uzmptshftfval  44799  iccdifprioo  45969  climisp  46197  limsupresxr  46217  liminfresxr  46218  dvnmul  46394  volico  46434  volioore  46441  fourierdlem74  46631  fourierdlem75  46632  sge0iunmptlemfi  46864  sge0iunmptlemre  46866  sge0iunmpt  46869  sge0xp  46880  hspmbllem2  47078  smflimlem3  47224  smfsupmpt  47266  smfinflem  47268  smfinfmpt  47270  smflimsupmpt  47280  smfliminfmpt  47283  funressnbrafv2  47715  uniimaelsetpreimafv  47879  imasetpreimafvbijlemfv1  47886  imasetpreimafvbijlemfo  47888  sprsymrelfo  47980  nnsum4primesodd  48295  nnsum4primesoddALTV  48296  grtrissvtx  48443  gricgrlic  48517  nn0mnd  48678  lcoss  48935  snlindsntorlem  48969  mreclat  49495  aacllem  50299