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  3212  vtocl3  3534  spc3egv  3564  moi2  3681  sbc3ie  3823  2if2  4545  preq12bg  4820  ralxfrd2  5385  reuhypd  5392  otsndisj  5504  funcnvqp  6604  fvtp1g  7202  fntpb  7214  f1imass  7267  weisoeq  7364  f1ofveu  7413  f1ocnvfv3  7414  funeldmdif  8051  curry1f  8107  curry2f  8109  funsssuppss  8192  frrlem13  8301  tfrlem11  8381  oalimcl  8551  oeordsuc  8586  oelim2  8587  nneob  8648  nadd4  8691  mapxpen  9138  findcard  9155  enfii  9177  domtrfil  9183  domnsymfi  9191  phplem2  9196  php  9198  wemaplem3  9517  en2eqpr  10007  infxpabs  10210  infxp  10213  cfflb  10258  cfsmolem  10269  isf32lem12  10363  fin1a2lem9  10407  fin1a2s  10413  axcc3  10437  axdc3lem4  10452  zornn0g  10504  pwfseqlem4  10664  tskwun  10786  tskint  10787  tskxp  10789  tskmap  10790  gruf  10813  grutsk1  10823  addcanpi  10901  ltapi  10905  mul4  11395  add4  11448  2addsub  11488  addsubeq4  11489  muladd  11663  ltleadd  11714  receu  11876  p1le  12077  mulgt1  12093  lbinf  12185  zdiv  12684  fzind  12712  fnn0ind  12713  fzindd  12716  uzss  12903  zbtwnre  12988  qmulcl  13009  qreccl  13011  xrlttr  13183  xaddass  13293  xmulasslem3  13330  xadddilem  13338  xrsupsslem  13351  xrinfmsslem  13352  supxrunb1  13363  ioo0  13415  ico0  13436  ioc0  13437  icc0  13438  iooshf  13471  prunioo  13526  ioojoin  13528  elfz5  13562  elfz0fzfz0  13680  elfzonelfzo  13817  fzind2  13836  modaddb  13962  mulexpz  14158  expsub  14166  digit1  14293  facndiv  14344  faclbnd4lem4  14352  faclbnd4  14353  faclbnd5  14354  bccmpl  14365  bcval5  14374  bcpasc  14377  hashunx  14442  hashunsnggt  14450  hashdmpropge2  14540  ccatrn  14647  swrdspsleq  14727  swrdccat2  14731  ccatpfx  14762  pfxccat1  14763  swrdswrd  14766  revpfxsfxrev  14829  cshf1  14873  crim  15192  absmax  15407  ello12r  15594  elo12r  15605  climshftlem  15651  2sumeq2dv  15781  hash2iun  15900  expcnv  15943  2cprodeq2dv  16004  rpnnen2lem7  16300  dvdsval3  16338  dvdsnegb  16355  muldvds1  16362  muldvds2  16363  dvdscmul  16364  dvdsmulc  16365  dvdsmulcr  16367  dvds2ln  16371  divalgb  16486  ndvdssub  16491  gcddiv  16633  lcmfval  16703  lcmfcl  16710  dvdslcmf  16713  rpexp1i  16806  phiprmpw  16859  hashgcdeq  16873  pythagtriplem1  16900  pockthg  16990  infpnlem1  16994  4sqlem3  17034  0ramcl  17107  firest  17509  imasaddfnlem  17606  imasleval  17619  mrerintcl  17673  iscatd  17753  fullestrcsetc  18231  fullsetcestrc  18246  clatleglb  18598  mreclatBAD  18643  pslem  18652  mndind  18926  grplmulf1o  19125  grplactcnv  19155  mulgnn0subcl  19199  mulgsubcl  19200  mulgdir  19218  issubg2  19254  issubgrpd2  19255  nmzsubg  19277  eqgen  19295  cycsubm  19319  cycsubgcl  19323  cycsubgss  19324  ghmmulg  19344  ghmf1  19362  kerf1ghm  19363  conjghm  19365  symgpssefmnd  19512  gsmsymgreqlem2  19547  symgfixfo  19555  odeq  19666  odval2  19667  odf1  19678  dfod2  19680  gexdvds  19700  gexdvds2  19701  gexcl2  19705  gexdvds3  19706  sylow2blem2  19737  efgsp1  19853  efgrelexlemb  19866  cmnbascntr  19921  mulgmhm  19943  mulgghm  19944  iscyggen2  19997  iscyg3  20002  ablsimpgfindlem1  20225  ogrpaddltbi  20255  srglmhm  20349  srgrmhm  20350  ringlghm  20443  ringrghm  20444  gsumdixp  20448  dvdsrcl2  20496  crngunit  20508  cntzsubrng  20718  subrgugrp  20742  cntzsubr  20757  rnghmsubcsetclem2  20783  rhmsubcsetclem2  20812  rhmsubcrngclem2  20818  sdrgacs  20956  lmodvsdir  21059  lmodvsass  21060  lmodvsghm  21096  lsssubg  21130  lss1d  21136  islbs2  21330  lidlsubg  21400  lidlsubcl  21401  rngqiprngimfo  21493  lpigen  21555  xrsdsreval  21614  expghm  21677  mulgghm2  21678  ip0r  21839  obs2ss  21931  islindf3  22028  scmatscm  22722  scmataddcl  22725  scmatsubcl  22726  scmatfo  22739  matunit  22887  cpmatelimp  22921  cpmatelimp2  22923  cpmatinvcl  22926  cpmatmcl  22928  mat2pmatf  22937  m2cpmf  22951  cpm2mf  22961  m2cpmfo  22965  m2cpminv  22969  decpmataa0  22977  pm2mpf  23007  pm2mpf1  23008  idpm2idmp  23010  pm2mpfo  23023  elcls2  23283  opnnei  23329  innei  23334  iscnp4  23472  cnpnei  23473  iscncl  23478  cnnei  23491  cnconst  23493  ordthauslem  23592  bwth  23619  1stccnp  23672  llyrest  23695  nllyrest  23696  kgenss  23753  xkoccn  23829  kqsat  23941  kqt0lem  23946  isr0  23947  fbssfi  24047  isfild  24068  filconn  24093  trfilss  24099  fgtr  24100  ufileu  24129  ufilen  24140  fmfnfmlem4  24167  fmfnfm  24168  hausflimi  24190  cnpflf2  24210  cnpflf  24211  cnpfcf  24251  cnextcn  24277  tsmsxplem1  24363  tsmsxp  24365  ustuqtop0  24450  ismeti  24535  isxmet2d  24537  elbl2ps  24599  elbl2  24600  xblpnfps  24605  xblpnf  24606  xbln0  24624  blin  24631  blssexps  24636  blssex  24637  blcls  24716  blsscls  24717  metrest  24734  metustbl  24776  psmetutop  24777  nmf2  24803  ngpi  24838  tngngp3  24866  nmdvr  24880  nmoi  24938  nmoix  24939  nmoleub  24941  nghmcn  24955  iccntr  25032  metdsle  25063  icoopnst  25151  iocopnst  25152  icccvx  25162  pi1xfr  25267  isclmi0  25310  iscvsi  25341  cphipval  25455  lmmbr  25470  lmmbr2  25471  iscfil3  25485  iscau2  25489  cfilres  25508  bcthlem1  25536  bcthlem4  25539  bcthlem5  25540  rrxmet  25620  ioombl  25777  iccvolcl  25779  ioovolcl  25782  mbfi1fseqlem3  25929  mbfi1fseqlem4  25930  mbfi1fseqlem5  25931  ig1pcl  26389  ig1prsp  26391  aannenlem1  26544  taylplem1  26579  dvtaylp  26586  relogeftb  26802  logdivlt  26839  cxpexp  26886  rpcxpcl  26894  isppw2  27332  vmappw  27333  lgslem4  27517  lgscllem  27521  lgsneg1  27539  lgsne0  27552  nosepdm  27901  sltsdisj  28049  mulcutlem  28377  ltonold  28507  zsoring  28655  bdayfinbndlem1  28713  z12bdaylem  28730  brbtwn2  29312  ax5seglem1  29335  ax5seglem2  29336  axcontlem4  29374  ewlkprop  30013  uspgr2wlkeq  30055  uhgrwkspthlem2  30169  clwlkclwwlkfo  30429  eupth2lem3lem7  30658  frgr3vlem2  30698  3cyclfrgrrn1  30709  4cycl2vnunb  30714  frgrncvvdeqlem8  30730  grpoidinvlem3  30931  isvciOLD  31005  nmcvcn  31120  ipval2lem2  31129  sspimsval  31163  isblo2  31208  nmoo0  31216  blocni  31230  isph  31247  hvadd4  31461  hiassdi  31516  ocsh  31708  chj4  31960  spansncol  31993  pjjsi  32125  hoscl  32170  hodcl  32172  hoadd4  32209  homco1  32226  homulass  32227  hoadddi  32228  hoadddir  32229  unoplin  32345  adjvalval  32362  hmoplin  32367  bralnfn  32373  brafnmul  32376  lnopmi  32425  lnopcoi  32428  hmops  32445  hmopm  32446  nmophmi  32456  lnfncnbd  32482  cnlnadjlem2  32493  adjlnop  32511  adjmul  32517  adjadd  32518  branmfn  32530  kbass5  32545  kbass6  32546  leop2  32549  leopadd  32557  leopmuli  32558  pjimai  32601  atcvatlem  32810  chirredlem2  32816  mdsymlem3  32830  mdsymlem5  32832  sumdmdii  32840  sumdmdlem  32843  cdj3lem2a  32861  cdj3lem2b  32862  cdj3lem3a  32864  cdj3i  32866  nn0difffzod  33221  xreceu  33313  cshwrnid  33347  toslublem  33358  tosglblem  33360  lmodvslmhm  33436  archiabllem1b  33578  archiabllem2c  33581  archiabl  33584  slmdvsdir  33602  slmdvsass  33603  grplsm0l  33778  pidlnzb  33796  rprmndvdsru  33885  mplvrpmmhm  34002  mplvrpmrhm  34003  zarcls1  34325  pstmxmet  34353  ordtconnlem1  34380  hasheuni  34541  omsf  34753  ballotlemirc  34989  signswmnd  35011  bnj1204  35467  fineqvac  35588  fisshasheq  35663  txpconn  35763  cvmscld  35804  satfbrsuc  35897  satfrnmapom  35901  satfun  35942  elmpps  36104  dfrdg2  36324  wsuclem  36354  segconeu  36542  linecom  36681  linethru  36684  lineintmo  36688  fnemeet2  36937  fnejoin2  36939  fvineqsneq  38117  lindsadd  38323  lindsdom  38324  lindsenlbs  38325  matunitlindflem1  38326  matunitlindflem2  38327  heicant  38365  mblfinlem1  38367  mblfinlem3  38369  ismblfin  38371  cnambfre  38378  itg2addnclem2  38382  ftc1anclem1  38403  ftc1anclem5  38407  ftc1anclem6  38408  ftc2nc  38412  areacirclem2  38419  areacirclem4  38421  areacirclem5  38422  areacirc  38423  fzmul  38452  subspopn  38463  isbndx  38493  isbnd2  38494  isbnd3  38495  ssbnd  38499  prdstotbnd  38505  heibor1  38521  rrnmet  38540  rngonegmn1l  38652  rngohomco  38685  rngoisocnv  38692  rngoisoco  38693  crngohomfo  38717  isidlc  38726  rngoidl  38735  prnc  38778  ispridlc  38781  cvrval2  40108  glbconxN  40212  hlrelat5N  40235  cvratlem  40255  cvrat2  40263  athgt  40290  3dim2  40302  llnn0  40350  lplnn0N  40381  lvoln0N  40425  snatpsubN  40584  paddasslem18  40671  pmod1i  40682  lhpexle2  40844  lhpexle3lem  40845  lhpexle3  40846  ldilcnv  40949  trlcnv  40999  trlnidatb  41011  cdleme32snaw  41269  cdleme32fvaw  41273  cdleme42ke  41319  cdlemeg46gf  41367  cdleme50trn12  41386  cdlemg1cex  41422  cdlemb3  41440  tgrpgrplem  41583  tgrpabl  41585  tendoplcl2  41612  tendo0pl  41625  tendoicl  41630  tendoipl  41631  cdlemkid3N  41767  tendoex  41809  erngdvlem4  41825  erngdvlem4-rN  41833  dib1dim  41999  dib1dim2  42002  dihglbcpreN  42134  dihmeetALTN  42161  dih1dimatlem  42163  dihatlat  42168  lcmineqlem1  42856  lcmineqlem3  42858  aks4d1p1  42903  aks4d1p7d1  42909  aks4d1p8  42914  sticksstones1  42973  sticksstones2  42974  sticksstones3  42975  sticksstones8  42980  sticksstones10  42982  sticksstones11  42983  sticksstones12a  42984  sticksstones12  42985  sticksstones17  42990  sticksstones19  42992  oddcomabszz  43731  acongtr  43765  rpnnen3lem  43818  islssfg  43857  lmhmfgsplit  43873  unxpwdom3  43882  hbtlem7  43912  iocmbl  44000  ss2iundf  44445  ismnu  45031  grumnudlem  45055  ismnushort  45071  nzss  45087  dvconstbi  45104  bccbc  45115  uzmptshftfval  45116  iccdifprioo  46292  climisp  46520  limsupresxr  46540  liminfresxr  46541  dvnmul  46717  volico  46757  volioore  46764  fourierdlem74  46954  fourierdlem75  46955  sge0iunmptlemfi  47187  sge0iunmptlemre  47189  sge0iunmpt  47192  sge0xp  47203  hspmbllem2  47401  smflimlem3  47547  smfsupmpt  47589  smfinflem  47591  smfinfmpt  47593  smflimsupmpt  47603  smfliminfmpt  47606  funressnbrafv2  48041  uniimaelsetpreimafv  48205  imasetpreimafvbijlemfv1  48212  imasetpreimafvbijlemfo  48214  sprsymrelfo  48306  nnsum4primesodd  48621  nnsum4primesoddALTV  48622  grtrissvtx  48769  gricgrlic  48843  nn0mnd  49003  lcoss  49275  snlindsntorlem  49309  mreclat  49834  aacllem  50680