Theorem 3expa 1117

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

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

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 206  df-3an 1088

This theorem is referenced by:  3exp  1118  ad4ant123  1171  ad4ant124  1172  ad4ant134  1173  ad4ant234  1174  ad5ant123  1363  3anidm23  1420  mp3an2  1448  mpd3an3  1461  rgen3  3122  vtocl3  3502  spc3egv  3543  moi2  3652  sbc3ie  3803  2if2  4515  preq12bg  4785  ralxfrd2  5336  reuhypd  5343  otsndisj  5434  funcnvqp  6505  fvtp1g  7082  fntpb  7094  f1imass  7146  weisoeq  7235  f1ofveu  7279  f1ocnvfv3  7280  funeldmdif  7898  curry1f  7955  curry2f  7957  funsssuppss  8015  frrlem13  8123  tfrlem11  8228  oalimcl  8400  oeordsuc  8434  oelim2  8435  nneob  8495  mapxpen  8939  findcard  8955  enfii  8981  domtrfil  8987  domnsymfi  8995  phplem2  9000  php  9002  wemaplem3  9316  en2eqpr  9772  infxpabs  9977  infxp  9980  cfflb  10024  cfsmolem  10035  isf32lem12  10129  fin1a2lem9  10173  fin1a2s  10179  axcc3  10203  axdc3lem4  10218  zornn0g  10270  pwfseqlem4  10427  tskwun  10549  tskint  10550  tskxp  10552  tskmap  10553  gruf  10576  grutsk1  10586  addcanpi  10664  ltapi  10668  mul4  11152  add4  11204  2addsub  11244  addsubeq4  11245  muladd  11416  ltleadd  11467  receu  11629  p1le  11829  lbinf  11937  zdiv  12399  fzind  12427  fnn0ind  12428  fzindd  12431  uzss  12614  zbtwnre  12695  qmulcl  12716  qreccl  12718  xrlttr  12883  xaddass  12992  xmulasslem3  13029  xadddilem  13037  xrsupsslem  13050  xrinfmsslem  13051  supxrunb1  13062  ioo0  13113  ico0  13134  ioc0  13135  icc0  13136  iooshf  13167  prunioo  13222  ioojoin  13224  elfz5  13257  elfz0fzfz0  13370  elfzonelfzo  13498  fzind2  13514  mulexpz  13832  expsub  13840  digit1  13961  facndiv  14011  faclbnd4lem4  14019  faclbnd4  14020  faclbnd5  14021  bccmpl  14032  bcval5  14041  bcpasc  14044  hashunx  14110  hashunsnggt  14118  hashdmpropge2  14206  ccatrn  14303  swrdspsleq  14387  swrdccat2  14391  ccatpfx  14423  pfxccat1  14424  swrdswrd  14427  cshf1  14532  crim  14835  absmax  15050  ello12r  15235  elo12r  15246  climshftlem  15292  2sumeq2dv  15426  hash2iun  15544  expcnv  15585  2cprodeq2dv  15644  rpnnen2lem7  15938  dvdsval3  15976  dvdsnegb  15992  muldvds1  15999  muldvds2  16000  dvdscmul  16001  dvdsmulc  16002  dvdsmulcr  16004  dvds2ln  16007  divalgb  16122  ndvdssub  16127  gcddiv  16268  lcmfval  16335  lcmfcl  16342  dvdslcmf  16345  rpexp1i  16437  phiprmpw  16486  hashgcdeq  16499  pythagtriplem1  16526  pockthg  16616  infpnlem1  16620  4sqlem3  16660  0ramcl  16733  firest  17152  imasaddfnlem  17248  imasleval  17261  mrerintcl  17315  iscatd  17391  fullestrcsetc  17877  fullsetcestrc  17892  clatleglb  18245  mreclatBAD  18290  pslem  18299  mndind  18475  grplmulf1o  18658  grplactcnv  18687  mulgnn0subcl  18726  mulgsubcl  18727  mulgdir  18744  issubg2  18779  issubgrpd2  18780  nmzsubg  18802  eqgen  18818  cycsubm  18830  cycsubgcl  18834  cycsubgss  18835  ghmmulg  18855  conjghm  18874  symgpssefmnd  19012  gsmsymgreqlem2  19048  symgfixfo  19056  odeq  19167  odval2  19168  odf1  19178  dfod2  19180  gexdvds  19198  gexdvds2  19199  gexcl2  19203  gexdvds3  19204  sylow2blem2  19235  efgsp1  19352  efgrelexlemb  19365  mulgmhm  19438  mulgghm  19439  iscyggen2  19490  iscyg3  19495  ablsimpgfindlem1  19719  srglmhm  19780  srgrmhm  19781  ringlghm  19852  ringrghm  19853  gsumdixp  19857  dvdsrcl2  19901  crngunit  19913  kerf1ghm  19996  subrgugrp  20052  cntzsubr  20066  sdrgacs  20078  lmodvsdir  20156  lmodvsass  20157  lmodvsghm  20193  lsssubg  20228  lss1d  20234  islbs2  20425  lidlsubg  20495  lidlsubcl  20496  quscrng  20520  lpigen  20536  xrsdsreval  20652  expghm  20706  mulgghm2  20707  ip0r  20851  obs2ss  20945  islindf3  21042  scmatscm  21671  scmataddcl  21674  scmatsubcl  21675  scmatfo  21688  matunit  21836  cpmatelimp  21870  cpmatelimp2  21872  cpmatinvcl  21875  cpmatmcl  21877  mat2pmatf  21886  m2cpmf  21900  cpm2mf  21910  m2cpmfo  21914  m2cpminv  21918  decpmataa0  21926  pm2mpf  21956  pm2mpf1  21957  idpm2idmp  21959  pm2mpfo  21972  elcls2  22234  opnnei  22280  innei  22285  iscnp4  22423  cnpnei  22424  iscncl  22429  cnnei  22442  cnconst  22444  ordthauslem  22543  bwth  22570  1stccnp  22622  llyrest  22645  nllyrest  22646  kgenss  22703  xkoccn  22779  kqsat  22891  kqt0lem  22896  isr0  22897  fbssfi  22997  isfild  23018  filconn  23043  trfilss  23049  fgtr  23050  ufileu  23079  ufilen  23090  fmfnfmlem4  23117  fmfnfm  23118  hausflimi  23140  cnpflf2  23160  cnpflf  23161  cnpfcf  23201  cnextcn  23227  tsmsxplem1  23313  tsmsxp  23315  ustuqtop0  23401  ismeti  23487  isxmet2d  23489  elbl2ps  23551  elbl2  23552  xblpnfps  23557  xblpnf  23558  xbln0  23576  blin  23583  blssexps  23588  blssex  23589  blcls  23671  blsscls  23672  metrest  23689  metustbl  23731  psmetutop  23732  nmf2  23758  ngpi  23793  tngngp3  23829  nmdvr  23843  nmoi  23901  nmoix  23902  nmoleub  23904  nghmcn  23918  iccntr  23993  metdsle  24024  icoopnst  24111  iocopnst  24112  icccvx  24122  pi1xfr  24227  isclmi0  24270  iscvsi  24301  cphipval  24416  lmmbr  24431  lmmbr2  24432  iscfil3  24446  iscau2  24450  cfilres  24469  bcthlem1  24497  bcthlem4  24500  bcthlem5  24501  rrxmet  24581  ioombl  24738  iccvolcl  24740  ioovolcl  24743  mbfi1fseqlem3  24891  mbfi1fseqlem4  24892  mbfi1fseqlem5  24893  ig1pcl  25349  ig1prsp  25351  aannenlem1  25497  taylplem1  25531  dvtaylp  25538  relogeftb  25749  logdivlt  25785  cxpexp  25832  rpcxpcl  25840  isppw2  26273  vmappw  26274  lgslem4  26457  lgscllem  26461  lgsneg1  26479  lgsne0  26492  brbtwn2  27282  ax5seglem1  27305  ax5seglem2  27306  axcontlem4  27344  ewlkprop  27979  uspgr2wlkeq  28022  uhgrwkspthlem2  28131  clwlkclwwlkfo  28382  eupth2lem3lem7  28607  frgr3vlem2  28647  3cyclfrgrrn1  28658  4cycl2vnunb  28663  frgrncvvdeqlem8  28679  grpoidinvlem3  28877  isvciOLD  28951  nmcvcn  29066  ipval2lem2  29075  sspimsval  29109  isblo2  29154  nmoo0  29162  blocni  29176  isph  29193  hvadd4  29407  hiassdi  29462  ocsh  29654  chj4  29906  spansncol  29939  pjjsi  30071  hoscl  30116  hodcl  30118  hoadd4  30155  homco1  30172  homulass  30173  hoadddi  30174  hoadddir  30175  unoplin  30291  adjvalval  30308  hmoplin  30313  bralnfn  30319  brafnmul  30322  lnopmi  30371  lnopcoi  30374  hmops  30391  hmopm  30392  nmophmi  30402  lnfncnbd  30428  cnlnadjlem2  30439  adjlnop  30457  adjmul  30463  adjadd  30464  branmfn  30476  kbass5  30491  kbass6  30492  leop2  30495  leopadd  30503  leopmuli  30504  pjimai  30547  atcvatlem  30756  chirredlem2  30762  mdsymlem3  30776  mdsymlem5  30778  sumdmdii  30786  sumdmdlem  30789  cdj3lem2a  30807  cdj3lem2b  30808  cdj3lem3a  30810  cdj3i  30812  xreceu  31205  cshwrnid  31242  toslublem  31259  tosglblem  31261  lmodvslmhm  31319  ogrpaddltbi  31353  archiabllem1b  31455  archiabllem2c  31458  archiabl  31461  slmdvsdir  31478  slmdvsass  31479  grplsm0l  31600  zarcls1  31828  pstmxmet  31856  ordtconnlem1  31883  hasheuni  32062  omsf  32272  ballotlemirc  32507  signswmnd  32545  bnj1204  33001  fineqvac  33075  fisshasheq  33082  revpfxsfxrev  33086  txpconn  33203  cvmscld  33244  satfbrsuc  33337  satfrnmapom  33341  satfun  33382  elmpps  33544  dfrdg2  33780  wsuclem  33828  nosepdm  33896  ssltdisj  34024  segconeu  34322  linecom  34461  linethru  34464  lineintmo  34468  fnemeet2  34565  fnejoin2  34567  fvineqsneq  35592  lindsadd  35779  lindsdom  35780  lindsenlbs  35781  matunitlindflem1  35782  matunitlindflem2  35783  heicant  35821  mblfinlem1  35823  mblfinlem3  35825  ismblfin  35827  cnambfre  35834  itg2addnclem2  35838  ftc1anclem1  35859  ftc1anclem5  35863  ftc1anclem6  35864  ftc2nc  35868  areacirclem2  35875  areacirclem4  35877  areacirclem5  35878  areacirc  35879  fzmul  35908  subspopn  35919  isbndx  35949  isbnd2  35950  isbnd3  35951  ssbnd  35955  prdstotbnd  35961  heibor1  35977  rrnmet  35996  rngonegmn1l  36108  rngohomco  36141  rngoisocnv  36148  rngoisoco  36149  crngohomfo  36173  isidlc  36182  rngoidl  36191  prnc  36234  ispridlc  36237  cvrval2  37295  glbconxN  37399  hlrelat5N  37422  cvratlem  37442  cvrat2  37450  athgt  37477  3dim2  37489  llnn0  37537  lplnn0N  37568  lvoln0N  37612  snatpsubN  37771  paddasslem18  37858  pmod1i  37869  lhpexle2  38031  lhpexle3lem  38032  lhpexle3  38033  ldilcnv  38136  trlcnv  38186  trlnidatb  38198  cdleme32snaw  38456  cdleme32fvaw  38460  cdleme42ke  38506  cdlemeg46gf  38554  cdleme50trn12  38573  cdlemg1cex  38609  cdlemb3  38627  tgrpgrplem  38770  tgrpabl  38772  tendoplcl2  38799  tendo0pl  38812  tendoicl  38817  tendoipl  38818  cdlemkid3N  38954  tendoex  38996  erngdvlem4  39012  erngdvlem4-rN  39020  dib1dim  39186  dib1dim2  39189  dihglbcpreN  39321  dihmeetALTN  39348  dih1dimatlem  39350  dihatlat  39355  lcmineqlem1  40044  lcmineqlem3  40046  aks4d1p1  40091  aks4d1p7d1  40097  aks4d1p8  40102  sticksstones1  40109  sticksstones2  40110  sticksstones3  40111  sticksstones8  40116  sticksstones10  40118  sticksstones11  40119  sticksstones12a  40120  sticksstones12  40121  sticksstones17  40126  sticksstones19  40128  metakunt29  40160  metakunt30  40161  metakunt31  40162  factwoffsmonot  40170  oddcomabszz  40773  acongtr  40807  rpnnen3lem  40860  islssfg  40902  lmhmfgsplit  40918  unxpwdom3  40927  hbtlem7  40957  iocmbl  41051  ss2iundf  41274  ismnu  41886  grumnudlem  41910  ismnushort  41926  nzss  41942  dvconstbi  41959  bccbc  41970  uzmptshftfval  41971  iccdifprioo  43061  climisp  43294  limsupresxr  43314  liminfresxr  43315  dvnmul  43491  volico  43531  volioore  43538  fourierdlem74  43728  fourierdlem75  43729  sge0iunmptlemfi  43958  sge0iunmptlemre  43960  sge0iunmpt  43963  sge0xp  43974  hspmbllem2  44172  smflimlem3  44318  smfsupmpt  44359  smfinflem  44361  smfinfmpt  44363  smflimsupmpt  44373  smfliminfmpt  44376  funressnbrafv2  44747  uniimaelsetpreimafv  44859  imasetpreimafvbijlemfv1  44866  imasetpreimafvbijlemfo  44868  sprsymrelfo  44960  nnsum4primesodd  45259  nnsum4primesoddALTV  45260  nn0mnd  45384  rnghmsubcsetclem2  45545  rhmsubcsetclem2  45591  rhmsubcrngclem2  45597  lcoss  45788  snlindsntorlem  45822  mreclat  46294  aacllem  46516