Theorem 3expa 1119

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-3an 1089

This theorem is referenced by:  3exp  1120  ad4ant123  1173  ad4ant124  1174  ad4ant134  1175  ad4ant234  1176  ad5ant123  1366  3anidm23  1423  mp3an2  1451  mpd3an3  1464  rgen3  3204  vtocl3  3567  spc3egv  3603  moi2  3722  sbc3ie  3868  2if2  4581  preq12bg  4853  ralxfrd2  5412  reuhypd  5419  otsndisj  5524  funcnvqp  6630  fvtp1g  7218  fntpb  7229  f1imass  7284  weisoeq  7375  f1ofveu  7425  f1ocnvfv3  7426  funeldmdif  8073  curry1f  8131  curry2f  8133  funsssuppss  8215  frrlem13  8323  tfrlem11  8428  oalimcl  8598  oeordsuc  8632  oelim2  8633  nneob  8694  nadd4  8736  mapxpen  9183  findcard  9203  enfii  9226  domtrfil  9232  domnsymfi  9240  phplem2  9245  php  9247  wemaplem3  9588  en2eqpr  10047  infxpabs  10251  infxp  10254  cfflb  10299  cfsmolem  10310  isf32lem12  10404  fin1a2lem9  10448  fin1a2s  10454  axcc3  10478  axdc3lem4  10493  zornn0g  10545  pwfseqlem4  10702  tskwun  10824  tskint  10825  tskxp  10827  tskmap  10828  gruf  10851  grutsk1  10861  addcanpi  10939  ltapi  10943  mul4  11429  add4  11482  2addsub  11522  addsubeq4  11523  muladd  11695  ltleadd  11746  receu  11908  p1le  12112  mulgt1  12129  lbinf  12221  zdiv  12688  fzind  12716  fnn0ind  12717  fzindd  12720  uzss  12901  zbtwnre  12988  qmulcl  13009  qreccl  13011  xrlttr  13182  xaddass  13291  xmulasslem3  13328  xadddilem  13336  xrsupsslem  13349  xrinfmsslem  13350  supxrunb1  13361  ioo0  13412  ico0  13433  ioc0  13434  icc0  13435  iooshf  13466  prunioo  13521  ioojoin  13523  elfz5  13556  elfz0fzfz0  13673  elfzonelfzo  13808  fzind2  13824  mulexpz  14143  expsub  14151  digit1  14276  facndiv  14327  faclbnd4lem4  14335  faclbnd4  14336  faclbnd5  14337  bccmpl  14348  bcval5  14357  bcpasc  14360  hashunx  14425  hashunsnggt  14433  hashdmpropge2  14522  ccatrn  14627  swrdspsleq  14703  swrdccat2  14707  ccatpfx  14739  pfxccat1  14740  swrdswrd  14743  cshf1  14848  crim  15154  absmax  15368  ello12r  15553  elo12r  15564  climshftlem  15610  2sumeq2dv  15741  hash2iun  15859  expcnv  15900  2cprodeq2dv  15961  rpnnen2lem7  16256  dvdsval3  16294  dvdsnegb  16311  muldvds1  16318  muldvds2  16319  dvdscmul  16320  dvdsmulc  16321  dvdsmulcr  16323  dvds2ln  16326  divalgb  16441  ndvdssub  16446  gcddiv  16588  lcmfval  16658  lcmfcl  16665  dvdslcmf  16668  rpexp1i  16760  phiprmpw  16813  hashgcdeq  16827  pythagtriplem1  16854  pockthg  16944  infpnlem1  16948  4sqlem3  16988  0ramcl  17061  firest  17477  imasaddfnlem  17573  imasleval  17586  mrerintcl  17640  iscatd  17716  fullestrcsetc  18196  fullsetcestrc  18211  clatleglb  18563  mreclatBAD  18608  pslem  18617  mndind  18841  grplmulf1o  19031  grplactcnv  19061  mulgnn0subcl  19105  mulgsubcl  19106  mulgdir  19124  issubg2  19159  issubgrpd2  19160  nmzsubg  19183  eqgen  19199  cycsubm  19220  cycsubgcl  19224  cycsubgss  19225  ghmmulg  19246  ghmf1  19264  kerf1ghm  19265  conjghm  19267  symgpssefmnd  19413  gsmsymgreqlem2  19449  symgfixfo  19457  odeq  19568  odval2  19569  odf1  19580  dfod2  19582  gexdvds  19602  gexdvds2  19603  gexcl2  19607  gexdvds3  19608  sylow2blem2  19639  efgsp1  19755  efgrelexlemb  19768  cmnbascntr  19823  mulgmhm  19845  mulgghm  19846  iscyggen2  19899  iscyg3  19904  ablsimpgfindlem1  20127  srglmhm  20218  srgrmhm  20219  ringlghm  20309  ringrghm  20310  gsumdixp  20316  dvdsrcl2  20366  crngunit  20378  cntzsubrng  20567  subrgugrp  20591  cntzsubr  20606  rnghmsubcsetclem2  20632  rhmsubcsetclem2  20661  rhmsubcrngclem2  20667  sdrgacs  20802  lmodvsdir  20884  lmodvsass  20885  lmodvsghm  20921  lsssubg  20955  lss1d  20961  islbs2  21156  lidlsubg  21233  lidlsubcl  21234  rngqiprngimfo  21311  lpigen  21345  xrsdsreval  21429  expghm  21486  mulgghm2  21487  ip0r  21655  obs2ss  21749  islindf3  21846  scmatscm  22519  scmataddcl  22522  scmatsubcl  22523  scmatfo  22536  matunit  22684  cpmatelimp  22718  cpmatelimp2  22720  cpmatinvcl  22723  cpmatmcl  22725  mat2pmatf  22734  m2cpmf  22748  cpm2mf  22758  m2cpmfo  22762  m2cpminv  22766  decpmataa0  22774  pm2mpf  22804  pm2mpf1  22805  idpm2idmp  22807  pm2mpfo  22820  elcls2  23082  opnnei  23128  innei  23133  iscnp4  23271  cnpnei  23272  iscncl  23277  cnnei  23290  cnconst  23292  ordthauslem  23391  bwth  23418  1stccnp  23470  llyrest  23493  nllyrest  23494  kgenss  23551  xkoccn  23627  kqsat  23739  kqt0lem  23744  isr0  23745  fbssfi  23845  isfild  23866  filconn  23891  trfilss  23897  fgtr  23898  ufileu  23927  ufilen  23938  fmfnfmlem4  23965  fmfnfm  23966  hausflimi  23988  cnpflf2  24008  cnpflf  24009  cnpfcf  24049  cnextcn  24075  tsmsxplem1  24161  tsmsxp  24163  ustuqtop0  24249  ismeti  24335  isxmet2d  24337  elbl2ps  24399  elbl2  24400  xblpnfps  24405  xblpnf  24406  xbln0  24424  blin  24431  blssexps  24436  blssex  24437  blcls  24519  blsscls  24520  metrest  24537  metustbl  24579  psmetutop  24580  nmf2  24606  ngpi  24641  tngngp3  24677  nmdvr  24691  nmoi  24749  nmoix  24750  nmoleub  24752  nghmcn  24766  iccntr  24843  metdsle  24874  icoopnst  24969  iocopnst  24970  icccvx  24981  pi1xfr  25088  isclmi0  25131  iscvsi  25162  cphipval  25277  lmmbr  25292  lmmbr2  25293  iscfil3  25307  iscau2  25311  cfilres  25330  bcthlem1  25358  bcthlem4  25361  bcthlem5  25362  rrxmet  25442  ioombl  25600  iccvolcl  25602  ioovolcl  25605  mbfi1fseqlem3  25752  mbfi1fseqlem4  25753  mbfi1fseqlem5  25754  ig1pcl  26218  ig1prsp  26220  aannenlem1  26370  taylplem1  26404  dvtaylp  26412  relogeftb  26626  logdivlt  26663  cxpexp  26710  rpcxpcl  26718  isppw2  27158  vmappw  27159  lgslem4  27344  lgscllem  27348  lgsneg1  27366  lgsne0  27379  nosepdm  27729  ssltdisj  27866  mulscutlem  28157  sltonold  28283  brbtwn2  28920  ax5seglem1  28943  ax5seglem2  28944  axcontlem4  28982  ewlkprop  29621  uspgr2wlkeq  29664  uhgrwkspthlem2  29774  clwlkclwwlkfo  30028  eupth2lem3lem7  30253  frgr3vlem2  30293  3cyclfrgrrn1  30304  4cycl2vnunb  30309  frgrncvvdeqlem8  30325  grpoidinvlem3  30525  isvciOLD  30599  nmcvcn  30714  ipval2lem2  30723  sspimsval  30757  isblo2  30802  nmoo0  30810  blocni  30824  isph  30841  hvadd4  31055  hiassdi  31110  ocsh  31302  chj4  31554  spansncol  31587  pjjsi  31719  hoscl  31764  hodcl  31766  hoadd4  31803  homco1  31820  homulass  31821  hoadddi  31822  hoadddir  31823  unoplin  31939  adjvalval  31956  hmoplin  31961  bralnfn  31967  brafnmul  31970  lnopmi  32019  lnopcoi  32022  hmops  32039  hmopm  32040  nmophmi  32050  lnfncnbd  32076  cnlnadjlem2  32087  adjlnop  32105  adjmul  32111  adjadd  32112  branmfn  32124  kbass5  32139  kbass6  32140  leop2  32143  leopadd  32151  leopmuli  32152  pjimai  32195  atcvatlem  32404  chirredlem2  32410  mdsymlem3  32424  mdsymlem5  32426  sumdmdii  32434  sumdmdlem  32437  cdj3lem2a  32455  cdj3lem2b  32456  cdj3lem3a  32458  cdj3i  32460  nn0difffzod  32808  xreceu  32904  cshwrnid  32946  toslublem  32962  tosglblem  32964  lmodvslmhm  33053  ogrpaddltbi  33095  archiabllem1b  33199  archiabllem2c  33202  archiabl  33205  slmdvsdir  33222  slmdvsass  33223  grplsm0l  33431  pidlnzb  33450  rprmndvdsru  33557  zarcls1  33868  pstmxmet  33896  ordtconnlem1  33923  hasheuni  34086  omsf  34298  ballotlemirc  34534  signswmnd  34572  bnj1204  35026  fineqvac  35111  fisshasheq  35120  revpfxsfxrev  35121  txpconn  35237  cvmscld  35278  satfbrsuc  35371  satfrnmapom  35375  satfun  35416  elmpps  35578  dfrdg2  35796  wsuclem  35826  segconeu  36012  linecom  36151  linethru  36154  lineintmo  36158  fnemeet2  36368  fnejoin2  36370  fvineqsneq  37413  lindsadd  37620  lindsdom  37621  lindsenlbs  37622  matunitlindflem1  37623  matunitlindflem2  37624  heicant  37662  mblfinlem1  37664  mblfinlem3  37666  ismblfin  37668  cnambfre  37675  itg2addnclem2  37679  ftc1anclem1  37700  ftc1anclem5  37704  ftc1anclem6  37705  ftc2nc  37709  areacirclem2  37716  areacirclem4  37718  areacirclem5  37719  areacirc  37720  fzmul  37748  subspopn  37759  isbndx  37789  isbnd2  37790  isbnd3  37791  ssbnd  37795  prdstotbnd  37801  heibor1  37817  rrnmet  37836  rngonegmn1l  37948  rngohomco  37981  rngoisocnv  37988  rngoisoco  37989  crngohomfo  38013  isidlc  38022  rngoidl  38031  prnc  38074  ispridlc  38077  cvrval2  39275  glbconxN  39380  hlrelat5N  39403  cvratlem  39423  cvrat2  39431  athgt  39458  3dim2  39470  llnn0  39518  lplnn0N  39549  lvoln0N  39593  snatpsubN  39752  paddasslem18  39839  pmod1i  39850  lhpexle2  40012  lhpexle3lem  40013  lhpexle3  40014  ldilcnv  40117  trlcnv  40167  trlnidatb  40179  cdleme32snaw  40437  cdleme32fvaw  40441  cdleme42ke  40487  cdlemeg46gf  40535  cdleme50trn12  40554  cdlemg1cex  40590  cdlemb3  40608  tgrpgrplem  40751  tgrpabl  40753  tendoplcl2  40780  tendo0pl  40793  tendoicl  40798  tendoipl  40799  cdlemkid3N  40935  tendoex  40977  erngdvlem4  40993  erngdvlem4-rN  41001  dib1dim  41167  dib1dim2  41170  dihglbcpreN  41302  dihmeetALTN  41329  dih1dimatlem  41331  dihatlat  41336  lcmineqlem1  42030  lcmineqlem3  42032  aks4d1p1  42077  aks4d1p7d1  42083  aks4d1p8  42088  sticksstones1  42147  sticksstones2  42148  sticksstones3  42149  sticksstones8  42154  sticksstones10  42156  sticksstones11  42157  sticksstones12a  42158  sticksstones12  42159  sticksstones17  42164  sticksstones19  42166  metakunt29  42234  metakunt30  42235  metakunt31  42236  factwoffsmonot  42243  oddcomabszz  42956  acongtr  42990  rpnnen3lem  43043  islssfg  43082  lmhmfgsplit  43098  unxpwdom3  43107  hbtlem7  43137  iocmbl  43225  ss2iundf  43672  ismnu  44280  grumnudlem  44304  ismnushort  44320  nzss  44336  dvconstbi  44353  bccbc  44364  uzmptshftfval  44365  iccdifprioo  45529  climisp  45761  limsupresxr  45781  liminfresxr  45782  dvnmul  45958  volico  45998  volioore  46005  fourierdlem74  46195  fourierdlem75  46196  sge0iunmptlemfi  46428  sge0iunmptlemre  46430  sge0iunmpt  46433  sge0xp  46444  hspmbllem2  46642  smflimlem3  46788  smfsupmpt  46830  smfinflem  46832  smfinfmpt  46834  smflimsupmpt  46844  smfliminfmpt  46847  funressnbrafv2  47256  uniimaelsetpreimafv  47383  imasetpreimafvbijlemfv1  47390  imasetpreimafvbijlemfo  47392  sprsymrelfo  47484  nnsum4primesodd  47783  nnsum4primesoddALTV  47784  uspgrimprop  47873  grtrissvtx  47911  gricgrlic  47978  nn0mnd  48095  lcoss  48353  snlindsntorlem  48387  mreclat  48886  aacllem  49320