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  3211  vtocl3  3531  spc3egv  3561  moi2  3677  sbc3ie  3820  2if2  4541  preq12bg  4811  ralxfrd2  5378  reuhypd  5385  otsndisj  5496  funcnvqp  6615  fvtp1g  7213  fntpb  7225  f1imass  7278  weisoeq  7375  f1ofveu  7424  f1ocnvfv3  7425  mpt3eqdv  7696  funeldmdif  8070  curry1f  8130  curry2f  8132  funsssuppss  8221  frrlem13  8330  tfrlem11  8410  oalimcl  8582  oeordsuc  8617  oelim2  8618  nneob  8679  nadd4  8722  mapxpen  9176  findcard  9193  enfii  9215  domtrfil  9221  domnsymfi  9229  phplem2  9234  php  9236  wemaplem3  9555  en2eqpr  10099  infxpabs  10302  infxp  10305  cfflb  10350  cfsmolem  10361  isf32lem12  10455  fin1a2lem9  10499  fin1a2s  10505  axcc3  10529  axdc3lem4  10544  zornn0g  10596  pwfseqlem4  10760  tskwun  10882  tskint  10883  tskxp  10885  tskmap  10886  gruf  10909  grutsk1  10919  addcanpi  10997  ltapi  11001  mul4  11491  add4  11544  2addsub  11584  addsubeq4  11585  muladd  11761  ltleadd  11812  receu  11974  p1le  12175  mulgt1  12191  lbinf  12283  zdiv  12782  fzind  12810  fnn0ind  12811  fzindd  12814  uzss  13001  zbtwnre  13086  qmulcl  13108  qreccl  13110  xrlttr  13282  xaddass  13392  xmulasslem3  13429  xadddilem  13437  xrsupsslem  13450  xrinfmsslem  13451  supxrunb1  13462  ioo0  13514  ico0  13535  ioc0  13536  icc0  13537  iooshf  13570  prunioo  13625  ioojoin  13627  elfz5  13661  elfz0fzfz0  13780  elfzonelfzo  13917  fzind2  13936  modaddb  14062  mulexpz  14258  expsub  14266  digit1  14394  facndiv  14445  faclbnd4lem4  14453  faclbnd4  14454  faclbnd5  14455  bccmpl  14466  bcval5  14475  bcpasc  14478  hashunx  14543  hashunsnggt  14551  hashdmpropge2  14641  ccatrn  14748  swrdspsleq  14829  swrdccat2  14833  ccatpfx  14864  pfxccat1  14865  swrdswrd  14868  revpfxsfxrev  14931  cshf1  14975  crim  15297  absmax  15512  ello12r  15699  elo12r  15710  climshftlem  15756  2sumeq2dv  15886  hash2iun  16005  expcnv  16048  2cprodeq2dv  16107  rpnnen2lem7  16403  dvdsval3  16441  dvdsnegb  16458  muldvds1  16465  muldvds2  16466  dvdscmul  16467  dvdsmulc  16468  dvdsmulcr  16470  dvds2ln  16474  divalgb  16589  ndvdssub  16594  gcddiv  16739  lcmfval  16811  lcmfcl  16818  dvdslcmf  16821  rpexp1i  16914  phiprmpw  16968  hashgcdeq  16982  pythagtriplem1  17009  pockthg  17099  infpnlem1  17103  4sqlem3  17143  0ramcl  17216  firest  17618  imasaddfnlem  17715  imasleval  17728  mrerintcl  17782  iscatd  17862  fullestrcsetc  18340  fullsetcestrc  18355  clatleglb  18707  mreclatBAD  18752  pslem  18761  mndind  19039  grplmulf1o  19238  grplactcnv  19268  mulgnn0subcl  19312  mulgsubcl  19313  mulgdir  19331  issubg2  19367  issubgrpd2  19368  nmzsubg  19390  eqgen  19408  cycsubm  19432  cycsubgcl  19436  cycsubgss  19437  ghmmulg  19457  ghmf1  19475  kerf1ghm  19476  conjghm  19478  symgpssefmnd  19625  gsmsymgreqlem2  19660  symgfixfo  19668  odeq  19779  odval2  19780  odf1  19791  dfod2  19793  gexdvds  19813  gexdvds2  19814  gexcl2  19818  gexdvds3  19819  sylow2blem2  19850  efgsp1  19966  efgrelexlemb  19979  cmnbascntr  20034  mulgmhm  20056  mulgghm  20057  iscyggen2  20110  iscyg3  20115  ablsimpgfindlem1  20338  ogrpaddltbi  20368  srglmhm  20462  srgrmhm  20463  ringlghm  20558  ringrghm  20559  gsumdixp  20563  dvdsrcl2  20611  crngunit  20623  cntzsubrng  20834  subrgugrp  20858  cntzsubr  20873  rnghmsubcsetclem2  20899  rhmsubcsetclem2  20928  rhmsubcrngclem2  20934  sdrgacs  21073  lmodvsdir  21176  lmodvsass  21177  lmodvsghm  21213  lsssubg  21247  lss1d  21253  islbs2  21447  lidlsubg  21517  lidlsubcl  21518  rngqiprngimfo  21612  lpigen  21674  xrsdsreval  21733  expghm  21796  mulgghm2  21797  ip0r  21958  obs2ss  22050  islindf3  22147  lindsdom  22171  lindsenlbs  22172  scmatscm  22843  scmataddcl  22846  scmatsubcl  22847  scmatfo  22860  matunit  23008  matunitlindflem1  23009  matunitlindflem2  23010  cpmatelimp  23045  cpmatelimp2  23047  cpmatinvcl  23050  cpmatmcl  23052  mat2pmatf  23061  m2cpmf  23075  cpm2mf  23085  m2cpmfo  23089  m2cpminv  23093  decpmataa0  23101  pm2mpf  23131  pm2mpf1  23132  idpm2idmp  23134  pm2mpfo  23147  elcls2  23407  opnnei  23453  innei  23458  iscnp4  23596  cnpnei  23597  iscncl  23602  cnnei  23615  cnconst  23617  ordthauslem  23716  bwth  23743  1stccnp  23796  llyrest  23819  nllyrest  23820  kgenss  23877  xkoccn  23953  kqsat  24065  kqt0lem  24070  isr0  24071  fbssfi  24171  isfild  24192  filconn  24217  trfilss  24223  fgtr  24224  ufileu  24253  ufilen  24264  fmfnfmlem4  24291  fmfnfm  24292  hausflimi  24314  cnpflf2  24334  cnpflf  24335  cnpfcf  24375  cnextcn  24401  tsmsxplem1  24487  tsmsxp  24489  ustuqtop0  24574  ismeti  24659  isxmet2d  24661  elbl2ps  24723  elbl2  24724  xblpnfps  24729  xblpnf  24730  xbln0  24748  blin  24755  blssexps  24760  blssex  24761  blcls  24840  blsscls  24841  metrest  24858  metustbl  24900  psmetutop  24901  nmf2  24927  ngpi  24962  tngngp3  24990  nmdvr  25004  nmoi  25062  nmoix  25063  nmoleub  25065  nghmcn  25079  iccntr  25156  metdsle  25187  icoopnst  25275  iocopnst  25276  icccvx  25286  pi1xfr  25391  isclmi0  25434  iscvsi  25465  cphipval  25579  lmmbr  25594  lmmbr2  25595  iscfil3  25609  iscau2  25613  cfilres  25632  bcthlem1  25660  bcthlem4  25663  bcthlem5  25664  rrxmet  25744  ioombl  25901  iccvolcl  25903  ioovolcl  25906  mbfi1fseqlem3  26053  mbfi1fseqlem4  26054  mbfi1fseqlem5  26055  ig1pcl  26512  ig1prsp  26514  aannenlem1  26670  taylplem1  26705  dvtaylp  26712  relogeftb  26927  logdivlt  26964  cxpexp  27011  rpcxpcl  27019  isppw2  27457  vmappw  27458  lgslem4  27642  lgscllem  27646  lgsneg1  27664  lgsne0  27677  nosepdm  28056  sltsdisj  28204  mulcutlem  28532  ltonold  28662  zsoring  28810  bdayfinbndlem1  28868  z12bdaylem  28885  brbtwn2  29498  ax5seglem1  29521  ax5seglem2  29522  axcontlem4  29560  ewlkprop  30199  uspgr2wlkeq  30241  uhgrwkspthlem2  30355  clwlkclwwlkfo  30615  eupth2lem3lem7  30850  frgr3vlem2  30890  3cyclfrgrrn1  30901  4cycl2vnunb  30906  frgrncvvdeqlem8  30922  grpoidinvlem3  31123  isvciOLD  31197  nmcvcn  31312  ipval2lem2  31321  sspimsval  31355  isblo2  31400  nmoo0  31408  blocni  31422  isph  31439  hvadd4  31653  hiassdi  31708  ocsh  31900  chj4  32152  spansncol  32185  pjjsi  32317  hoscl  32362  hodcl  32364  hoadd4  32401  homco1  32418  homulass  32419  hoadddi  32420  hoadddir  32421  unoplin  32537  adjvalval  32554  hmoplin  32559  bralnfn  32565  brafnmul  32568  lnopmi  32617  lnopcoi  32620  hmops  32637  hmopm  32638  nmophmi  32648  lnfncnbd  32674  cnlnadjlem2  32685  adjlnop  32703  adjmul  32709  adjadd  32710  branmfn  32722  kbass5  32737  kbass6  32738  leop2  32741  leopadd  32749  leopmuli  32750  pjimai  32793  atcvatlem  33002  chirredlem2  33008  mdsymlem3  33022  mdsymlem5  33024  sumdmdii  33032  sumdmdlem  33035  cdj3lem2a  33053  cdj3lem2b  33054  cdj3lem3a  33056  cdj3i  33058  nn0difffzod  33452  xreceu  33544  cshwrnid  33578  toslublem  33589  tosglblem  33591  lmodvslmhm  33667  archiabllem1b  33809  archiabllem2c  33812  archiabl  33815  slmdvsdir  33833  slmdvsass  33834  grplsm0l  34010  pidlnzb  34028  rprmndvdsru  34117  mplvrpmmhm  34234  mplvrpmrhm  34235  zarcls1  34557  pstmxmet  34585  ordtconnlem1  34612  hasheuni  34773  omsf  34984  ballotlemirc  35220  signswmnd  35242  bnj1204  35698  fineqvac  35858  fisshasheq  36017  txpconn  36121  cvmscld  36162  satfbrsuc  36255  satfrnmapom  36259  satfun  36300  elmpps  36462  dfrdg2  36687  wsuclem  36717  segconeu  36906  linecom  37045  linethru  37048  lineintmo  37052  fnemeet2  37285  fnejoin2  37287  fvineqsneq  38478  lindsadd  38679  heicant  38716  mblfinlem1  38718  mblfinlem3  38720  ismblfin  38722  cnambfre  38729  itg2addnclem2  38733  ftc1anclem1  38754  ftc1anclem5  38758  ftc1anclem6  38759  ftc2nc  38763  areacirclem2  38770  areacirclem4  38772  areacirclem5  38773  areacirc  38774  fzmul  38818  subspopn  38829  isbndx  38859  isbnd2  38860  isbnd3  38861  ssbnd  38865  prdstotbnd  38871  heibor1  38887  rrnmet  38906  rngonegmn1l  39018  rngohomco  39051  rngoisocnv  39058  rngoisoco  39059  crngohomfo  39083  isidlc  39092  rngoidl  39101  prnc  39144  ispridlc  39147  cvrval2  40474  glbconxN  40578  hlrelat5N  40601  cvratlem  40621  cvrat2  40629  athgt  40656  3dim2  40668  llnn0  40716  lplnn0N  40747  lvoln0N  40791  snatpsubN  40950  paddasslem18  41037  pmod1i  41048  lhpexle2  41210  lhpexle3lem  41211  lhpexle3  41212  ldilcnv  41315  trlcnv  41365  trlnidatb  41377  cdleme32snaw  41635  cdleme32fvaw  41639  cdleme42ke  41685  cdlemeg46gf  41733  cdleme50trn12  41752  cdlemg1cex  41788  cdlemb3  41806  tgrpgrplem  41949  tgrpabl  41951  tendoplcl2  41978  tendo0pl  41991  tendoicl  41996  tendoipl  41997  cdlemkid3N  42133  tendoex  42175  erngdvlem4  42191  erngdvlem4-rN  42199  dib1dim  42365  dib1dim2  42368  dihglbcpreN  42500  dihmeetALTN  42527  dih1dimatlem  42529  dihatlat  42534  lcmineqlem1  43222  lcmineqlem3  43224  aks4d1p1  43269  aks4d1p7d1  43275  aks4d1p8  43280  sticksstones1  43339  sticksstones2  43340  sticksstones3  43341  sticksstones8  43346  sticksstones10  43348  sticksstones11  43349  sticksstones12a  43350  sticksstones12  43351  sticksstones17  43356  sticksstones19  43358  oddcomabszz  44094  acongtr  44128  rpnnen3lem  44181  islssfg  44215  lmhmfgsplit  44231  unxpwdom3  44240  hbtlem7  44270  iocmbl  44358  ss2iundf  44802  ismnu  45388  grumnudlem  45412  ismnushort  45428  nzss  45444  dvconstbi  45461  bccbc  45472  uzmptshftfval  45473  iccdifprioo  46670  climisp  46898  limsupresxr  46918  liminfresxr  46919  dvnmul  47095  volico  47135  volioore  47142  fourierdlem74  47332  fourierdlem75  47333  sge0iunmptlemfi  47565  sge0iunmptlemre  47567  sge0iunmpt  47570  sge0xp  47581  hspmbllem2  47779  smflimlem3  47925  smfsupmpt  47967  smfinflem  47969  smfinfmpt  47971  smflimsupmpt  47981  smfliminfmpt  47984  funressnbrafv2  48456  uniimaelsetpreimafv  48620  imasetpreimafvbijlemfv1  48627  imasetpreimafvbijlemfo  48629  sprsymrelfo  48721  nnsum4primesodd  49036  nnsum4primesoddALTV  49037  grtrissvtx  49184  gricgrlic  49258  nn0mnd  49418  lcoss  49690  snlindsntorlem  49724  mreclat  50253  aacllem  51156