Theorem 3expa 1136

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-3an 1105

This theorem is used by:  3exp  1137  ad4ant123  1191  ad4ant124  1192  ad4ant134  1193  ad4ant234  1194  ad5ant123  1387  ad5ant124  1388  ad5ant125  1390  3anidm23  1448  mp3an2  1478  mpd3an3  1491  rgen3  3208  vtocl3  3528  spc3egv  3558  moi2  3674  sbc3ie  3816  2if2  4538  preq12bg  4813  ralxfrd2  5374  reuhypd  5381  otsndisj  5492  funcnvqp  6604  fvtp1g  7203  fntpb  7215  f1imass  7268  weisoeq  7365  f1ofveu  7414  f1ocnvfv3  7415  mpt3eqdv  7686  funeldmdif  8059  curry1f  8117  curry2f  8119  funsssuppss  8207  frrlem13  8316  tfrlem11  8396  oalimcl  8568  oeordsuc  8603  oelim2  8604  nneob  8665  nadd4  8708  mapxpen  9162  findcard  9179  enfii  9201  domtrfil  9207  domnsymfi  9215  phplem2  9220  php  9222  wemaplem3  9542  en2eqpr  10086  infxpabs  10289  infxp  10292  cfflb  10337  cfsmolem  10348  isf32lem12  10442  fin1a2lem9  10486  fin1a2s  10492  axcc3  10516  axdc3lem4  10531  zornn0g  10583  pwfseqlem4  10747  tskwun  10869  tskint  10870  tskxp  10872  tskmap  10873  gruf  10896  grutsk1  10906  addcanpi  10984  ltapi  10988  mul4  11478  add4  11531  2addsub  11571  addsubeq4  11572  muladd  11748  ltleadd  11799  receu  11961  p1le  12162  mulgt1  12178  lbinf  12270  zdiv  12769  fzind  12797  fnn0ind  12798  fzindd  12801  uzss  12988  zbtwnre  13073  qmulcl  13095  qreccl  13097  xrlttr  13269  xaddass  13379  xmulasslem3  13416  xadddilem  13424  xrsupsslem  13437  xrinfmsslem  13438  supxrunb1  13449  ioo0  13501  ico0  13522  ioc0  13523  icc0  13524  iooshf  13557  prunioo  13612  ioojoin  13614  elfz5  13648  elfz0fzfz0  13767  elfzonelfzo  13904  fzind2  13923  modaddb  14049  mulexpz  14245  expsub  14253  digit1  14381  facndiv  14432  faclbnd4lem4  14440  faclbnd4  14441  faclbnd5  14442  bccmpl  14453  bcval5  14462  bcpasc  14465  hashunx  14530  hashunsnggt  14538  hashdmpropge2  14628  ccatrn  14735  swrdspsleq  14815  swrdccat2  14819  ccatpfx  14850  pfxccat1  14851  swrdswrd  14854  revpfxsfxrev  14917  cshf1  14961  crim  15282  absmax  15497  ello12r  15684  elo12r  15695  climshftlem  15741  2sumeq2dv  15871  hash2iun  15990  expcnv  16033  2cprodeq2dv  16092  rpnnen2lem7  16388  dvdsval3  16426  dvdsnegb  16443  muldvds1  16450  muldvds2  16451  dvdscmul  16452  dvdsmulc  16453  dvdsmulcr  16455  dvds2ln  16459  divalgb  16574  ndvdssub  16579  gcddiv  16724  lcmfval  16796  lcmfcl  16803  dvdslcmf  16806  rpexp1i  16899  phiprmpw  16953  hashgcdeq  16967  pythagtriplem1  16994  pockthg  17084  infpnlem1  17088  4sqlem3  17128  0ramcl  17201  firest  17603  imasaddfnlem  17700  imasleval  17713  mrerintcl  17767  iscatd  17847  fullestrcsetc  18325  fullsetcestrc  18340  clatleglb  18692  mreclatBAD  18737  pslem  18746  mndind  19024  grplmulf1o  19223  grplactcnv  19253  mulgnn0subcl  19297  mulgsubcl  19298  mulgdir  19316  issubg2  19352  issubgrpd2  19353  nmzsubg  19375  eqgen  19393  cycsubm  19417  cycsubgcl  19421  cycsubgss  19422  ghmmulg  19442  ghmf1  19460  kerf1ghm  19461  conjghm  19463  symgpssefmnd  19610  gsmsymgreqlem2  19645  symgfixfo  19653  odeq  19764  odval2  19765  odf1  19776  dfod2  19778  gexdvds  19798  gexdvds2  19799  gexcl2  19803  gexdvds3  19804  sylow2blem2  19835  efgsp1  19951  efgrelexlemb  19964  cmnbascntr  20019  mulgmhm  20041  mulgghm  20042  iscyggen2  20095  iscyg3  20100  ablsimpgfindlem1  20323  ogrpaddltbi  20353  srglmhm  20447  srgrmhm  20448  ringlghm  20543  ringrghm  20544  gsumdixp  20548  dvdsrcl2  20596  crngunit  20608  cntzsubrng  20819  subrgugrp  20843  cntzsubr  20858  rnghmsubcsetclem2  20884  rhmsubcsetclem2  20913  rhmsubcrngclem2  20919  sdrgacs  21058  lmodvsdir  21161  lmodvsass  21162  lmodvsghm  21198  lsssubg  21232  lss1d  21238  islbs2  21432  lidlsubg  21502  lidlsubcl  21503  rngqiprngimfo  21597  lpigen  21659  xrsdsreval  21718  expghm  21781  mulgghm2  21782  ip0r  21943  obs2ss  22035  islindf3  22132  lindsdom  22156  lindsenlbs  22157  scmatscm  22828  scmataddcl  22831  scmatsubcl  22832  scmatfo  22845  matunit  22993  matunitlindflem1  22994  matunitlindflem2  22995  cpmatelimp  23030  cpmatelimp2  23032  cpmatinvcl  23035  cpmatmcl  23037  mat2pmatf  23046  m2cpmf  23060  cpm2mf  23070  m2cpmfo  23074  m2cpminv  23078  decpmataa0  23086  pm2mpf  23116  pm2mpf1  23117  idpm2idmp  23119  pm2mpfo  23132  elcls2  23392  opnnei  23438  innei  23443  iscnp4  23581  cnpnei  23582  iscncl  23587  cnnei  23600  cnconst  23602  ordthauslem  23701  bwth  23728  1stccnp  23781  llyrest  23804  nllyrest  23805  kgenss  23862  xkoccn  23938  kqsat  24050  kqt0lem  24055  isr0  24056  fbssfi  24156  isfild  24177  filconn  24202  trfilss  24208  fgtr  24209  ufileu  24238  ufilen  24249  fmfnfmlem4  24276  fmfnfm  24277  hausflimi  24299  cnpflf2  24319  cnpflf  24320  cnpfcf  24360  cnextcn  24386  tsmsxplem1  24472  tsmsxp  24474  ustuqtop0  24559  ismeti  24644  isxmet2d  24646  elbl2ps  24708  elbl2  24709  xblpnfps  24714  xblpnf  24715  xbln0  24733  blin  24740  blssexps  24745  blssex  24746  blcls  24825  blsscls  24826  metrest  24843  metustbl  24885  psmetutop  24886  nmf2  24912  ngpi  24947  tngngp3  24975  nmdvr  24989  nmoi  25047  nmoix  25048  nmoleub  25050  nghmcn  25064  iccntr  25141  metdsle  25172  icoopnst  25260  iocopnst  25261  icccvx  25271  pi1xfr  25376  isclmi0  25419  iscvsi  25450  cphipval  25564  lmmbr  25579  lmmbr2  25580  iscfil3  25594  iscau2  25598  cfilres  25617  bcthlem1  25645  bcthlem4  25648  bcthlem5  25649  rrxmet  25729  ioombl  25886  iccvolcl  25888  ioovolcl  25891  mbfi1fseqlem3  26038  mbfi1fseqlem4  26039  mbfi1fseqlem5  26040  ig1pcl  26497  ig1prsp  26499  aannenlem1  26655  taylplem1  26690  dvtaylp  26697  relogeftb  26912  logdivlt  26949  cxpexp  26996  rpcxpcl  27004  isppw2  27442  vmappw  27443  lgslem4  27627  lgscllem  27631  lgsneg1  27649  lgsne0  27662  nosepdm  28041  sltsdisj  28189  mulcutlem  28517  ltonold  28647  zsoring  28795  bdayfinbndlem1  28853  z12bdaylem  28870  brbtwn2  29483  ax5seglem1  29506  ax5seglem2  29507  axcontlem4  29545  ewlkprop  30184  uspgr2wlkeq  30226  uhgrwkspthlem2  30340  clwlkclwwlkfo  30600  eupth2lem3lem7  30835  frgr3vlem2  30875  3cyclfrgrrn1  30886  4cycl2vnunb  30891  frgrncvvdeqlem8  30907  grpoidinvlem3  31108  isvciOLD  31182  nmcvcn  31297  ipval2lem2  31306  sspimsval  31340  isblo2  31385  nmoo0  31393  blocni  31407  isph  31424  hvadd4  31638  hiassdi  31693  ocsh  31885  chj4  32137  spansncol  32170  pjjsi  32302  hoscl  32347  hodcl  32349  hoadd4  32386  homco1  32403  homulass  32404  hoadddi  32405  hoadddir  32406  unoplin  32522  adjvalval  32539  hmoplin  32544  bralnfn  32550  brafnmul  32553  lnopmi  32602  lnopcoi  32605  hmops  32622  hmopm  32623  nmophmi  32633  lnfncnbd  32659  cnlnadjlem2  32670  adjlnop  32688  adjmul  32694  adjadd  32695  branmfn  32707  kbass5  32722  kbass6  32723  leop2  32726  leopadd  32734  leopmuli  32735  pjimai  32778  atcvatlem  32987  chirredlem2  32993  mdsymlem3  33007  mdsymlem5  33009  sumdmdii  33017  sumdmdlem  33020  cdj3lem2a  33038  cdj3lem2b  33039  cdj3lem3a  33041  cdj3i  33043  nn0difffzod  33396  xreceu  33488  cshwrnid  33522  toslublem  33533  tosglblem  33535  lmodvslmhm  33611  archiabllem1b  33753  archiabllem2c  33756  archiabl  33759  slmdvsdir  33777  slmdvsass  33778  grplsm0l  33954  pidlnzb  33972  rprmndvdsru  34061  mplvrpmmhm  34178  mplvrpmrhm  34179  zarcls1  34501  pstmxmet  34529  ordtconnlem1  34556  hasheuni  34717  omsf  34928  ballotlemirc  35164  signswmnd  35186  bnj1204  35642  fineqvac  35784  fisshasheq  35903  txpconn  35997  cvmscld  36038  satfbrsuc  36131  satfrnmapom  36135  satfun  36176  elmpps  36338  dfrdg2  36557  wsuclem  36587  segconeu  36776  linecom  36915  linethru  36918  lineintmo  36922  fnemeet2  37155  fnejoin2  37157  fvineqsneq  38335  lindsadd  38536  heicant  38573  mblfinlem1  38575  mblfinlem3  38577  ismblfin  38579  cnambfre  38586  itg2addnclem2  38590  ftc1anclem1  38611  ftc1anclem5  38615  ftc1anclem6  38616  ftc2nc  38620  areacirclem2  38627  areacirclem4  38629  areacirclem5  38630  areacirc  38631  fzmul  38675  subspopn  38686  isbndx  38716  isbnd2  38717  isbnd3  38718  ssbnd  38722  prdstotbnd  38728  heibor1  38744  rrnmet  38763  rngonegmn1l  38875  rngohomco  38908  rngoisocnv  38915  rngoisoco  38916  crngohomfo  38940  isidlc  38949  rngoidl  38958  prnc  39001  ispridlc  39004  cvrval2  40331  glbconxN  40435  hlrelat5N  40458  cvratlem  40478  cvrat2  40486  athgt  40513  3dim2  40525  llnn0  40573  lplnn0N  40604  lvoln0N  40648  snatpsubN  40807  paddasslem18  40894  pmod1i  40905  lhpexle2  41067  lhpexle3lem  41068  lhpexle3  41069  ldilcnv  41172  trlcnv  41222  trlnidatb  41234  cdleme32snaw  41492  cdleme32fvaw  41496  cdleme42ke  41542  cdlemeg46gf  41590  cdleme50trn12  41609  cdlemg1cex  41645  cdlemb3  41663  tgrpgrplem  41806  tgrpabl  41808  tendoplcl2  41835  tendo0pl  41848  tendoicl  41853  tendoipl  41854  cdlemkid3N  41990  tendoex  42032  erngdvlem4  42048  erngdvlem4-rN  42056  dib1dim  42222  dib1dim2  42225  dihglbcpreN  42357  dihmeetALTN  42384  dih1dimatlem  42386  dihatlat  42391  lcmineqlem1  43079  lcmineqlem3  43081  aks4d1p1  43126  aks4d1p7d1  43132  aks4d1p8  43137  sticksstones1  43196  sticksstones2  43197  sticksstones3  43198  sticksstones8  43203  sticksstones10  43205  sticksstones11  43206  sticksstones12a  43207  sticksstones12  43208  sticksstones17  43213  sticksstones19  43215  oddcomabszz  43950  acongtr  43984  rpnnen3lem  44037  islssfg  44071  lmhmfgsplit  44087  unxpwdom3  44096  hbtlem7  44126  iocmbl  44214  ss2iundf  44658  ismnu  45244  grumnudlem  45268  ismnushort  45284  nzss  45300  dvconstbi  45317  bccbc  45328  uzmptshftfval  45329  iccdifprioo  46527  climisp  46755  limsupresxr  46775  liminfresxr  46776  dvnmul  46952  volico  46992  volioore  46999  fourierdlem74  47189  fourierdlem75  47190  sge0iunmptlemfi  47422  sge0iunmptlemre  47424  sge0iunmpt  47427  sge0xp  47438  hspmbllem2  47636  smflimlem3  47782  smfsupmpt  47824  smfinflem  47826  smfinfmpt  47828  smflimsupmpt  47838  smfliminfmpt  47841  funressnbrafv2  48313  uniimaelsetpreimafv  48477  imasetpreimafvbijlemfv1  48484  imasetpreimafvbijlemfo  48486  sprsymrelfo  48578  nnsum4primesodd  48893  nnsum4primesoddALTV  48894  grtrissvtx  49041  gricgrlic  49115  nn0mnd  49275  lcoss  49547  snlindsntorlem  49581  mreclat  50104  aacllem  50938