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 1090	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		3exp.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	1, 2	sylbir 234	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 1090

This theorem is referenced by:  3exp  1120  ad4ant123  1173  ad4ant124  1174  ad4ant134  1175  ad4ant234  1176  ad5ant123  1365  3anidm23  1422  mp3an2  1450  mpd3an3  1463  rgen3  3203  vtocl3  3553  spc3egv  3594  moi2  3712  sbc3ie  3863  2if2  4583  preq12bg  4854  ralxfrd2  5410  reuhypd  5417  otsndisj  5519  funcnvqp  6610  fvtp1g  7196  fntpb  7208  f1imass  7260  weisoeq  7349  f1ofveu  7400  f1ocnvfv3  7401  funeldmdif  8031  curry1f  8089  curry2f  8091  funsssuppss  8172  frrlem13  8280  tfrlem11  8385  oalimcl  8557  oeordsuc  8591  oelim2  8592  nneob  8652  nadd4  8694  mapxpen  9140  findcard  9160  enfii  9186  domtrfil  9192  domnsymfi  9200  phplem2  9205  php  9207  wemaplem3  9540  en2eqpr  9999  infxpabs  10204  infxp  10207  cfflb  10251  cfsmolem  10262  isf32lem12  10356  fin1a2lem9  10400  fin1a2s  10406  axcc3  10430  axdc3lem4  10445  zornn0g  10497  pwfseqlem4  10654  tskwun  10776  tskint  10777  tskxp  10779  tskmap  10780  gruf  10803  grutsk1  10813  addcanpi  10891  ltapi  10895  mul4  11379  add4  11431  2addsub  11471  addsubeq4  11472  muladd  11643  ltleadd  11694  receu  11856  p1le  12056  lbinf  12164  zdiv  12629  fzind  12657  fnn0ind  12658  fzindd  12661  uzss  12842  zbtwnre  12927  qmulcl  12948  qreccl  12950  xrlttr  13116  xaddass  13225  xmulasslem3  13262  xadddilem  13270  xrsupsslem  13283  xrinfmsslem  13284  supxrunb1  13295  ioo0  13346  ico0  13367  ioc0  13368  icc0  13369  iooshf  13400  prunioo  13455  ioojoin  13457  elfz5  13490  elfz0fzfz0  13603  elfzonelfzo  13731  fzind2  13747  mulexpz  14065  expsub  14073  digit1  14197  facndiv  14245  faclbnd4lem4  14253  faclbnd4  14254  faclbnd5  14255  bccmpl  14266  bcval5  14275  bcpasc  14278  hashunx  14343  hashunsnggt  14351  hashdmpropge2  14441  ccatrn  14536  swrdspsleq  14612  swrdccat2  14616  ccatpfx  14648  pfxccat1  14649  swrdswrd  14652  cshf1  14757  crim  15059  absmax  15273  ello12r  15458  elo12r  15469  climshftlem  15515  2sumeq2dv  15648  hash2iun  15766  expcnv  15807  2cprodeq2dv  15866  rpnnen2lem7  16160  dvdsval3  16198  dvdsnegb  16214  muldvds1  16221  muldvds2  16222  dvdscmul  16223  dvdsmulc  16224  dvdsmulcr  16226  dvds2ln  16229  divalgb  16344  ndvdssub  16349  gcddiv  16490  lcmfval  16555  lcmfcl  16562  dvdslcmf  16565  rpexp1i  16657  phiprmpw  16706  hashgcdeq  16719  pythagtriplem1  16746  pockthg  16836  infpnlem1  16840  4sqlem3  16880  0ramcl  16953  firest  17375  imasaddfnlem  17471  imasleval  17484  mrerintcl  17538  iscatd  17614  fullestrcsetc  18100  fullsetcestrc  18115  clatleglb  18468  mreclatBAD  18513  pslem  18522  mndind  18706  grplmulf1o  18894  grplactcnv  18923  mulgnn0subcl  18962  mulgsubcl  18963  mulgdir  18981  issubg2  19016  issubgrpd2  19017  nmzsubg  19040  eqgen  19056  cycsubm  19074  cycsubgcl  19078  cycsubgss  19079  ghmmulg  19099  conjghm  19118  symgpssefmnd  19258  gsmsymgreqlem2  19294  symgfixfo  19302  odeq  19413  odval2  19414  odf1  19425  dfod2  19427  gexdvds  19447  gexdvds2  19448  gexcl2  19452  gexdvds3  19453  sylow2blem2  19484  efgsp1  19600  efgrelexlemb  19613  cmnbascntr  19668  mulgmhm  19690  mulgghm  19691  iscyggen2  19744  iscyg3  19749  ablsimpgfindlem1  19972  srglmhm  20038  srgrmhm  20039  ringlghm  20118  ringrghm  20119  gsumdixp  20125  dvdsrcl2  20173  crngunit  20185  kerf1ghm  20275  subrgugrp  20375  cntzsubr  20391  sdrgacs  20410  lmodvsdir  20489  lmodvsass  20490  lmodvsghm  20526  lsssubg  20561  lss1d  20567  islbs2  20760  lidlsubg  20831  lidlsubcl  20832  quscrng  20871  lpigen  20887  xrsdsreval  20983  expghm  21037  mulgghm2  21038  ip0r  21182  obs2ss  21276  islindf3  21373  scmatscm  22007  scmataddcl  22010  scmatsubcl  22011  scmatfo  22024  matunit  22172  cpmatelimp  22206  cpmatelimp2  22208  cpmatinvcl  22211  cpmatmcl  22213  mat2pmatf  22222  m2cpmf  22236  cpm2mf  22246  m2cpmfo  22250  m2cpminv  22254  decpmataa0  22262  pm2mpf  22292  pm2mpf1  22293  idpm2idmp  22295  pm2mpfo  22308  elcls2  22570  opnnei  22616  innei  22621  iscnp4  22759  cnpnei  22760  iscncl  22765  cnnei  22778  cnconst  22780  ordthauslem  22879  bwth  22906  1stccnp  22958  llyrest  22981  nllyrest  22982  kgenss  23039  xkoccn  23115  kqsat  23227  kqt0lem  23232  isr0  23233  fbssfi  23333  isfild  23354  filconn  23379  trfilss  23385  fgtr  23386  ufileu  23415  ufilen  23426  fmfnfmlem4  23453  fmfnfm  23454  hausflimi  23476  cnpflf2  23496  cnpflf  23497  cnpfcf  23537  cnextcn  23563  tsmsxplem1  23649  tsmsxp  23651  ustuqtop0  23737  ismeti  23823  isxmet2d  23825  elbl2ps  23887  elbl2  23888  xblpnfps  23893  xblpnf  23894  xbln0  23912  blin  23919  blssexps  23924  blssex  23925  blcls  24007  blsscls  24008  metrest  24025  metustbl  24067  psmetutop  24068  nmf2  24094  ngpi  24129  tngngp3  24165  nmdvr  24179  nmoi  24237  nmoix  24238  nmoleub  24240  nghmcn  24254  iccntr  24329  metdsle  24360  icoopnst  24447  iocopnst  24448  icccvx  24458  pi1xfr  24563  isclmi0  24606  iscvsi  24637  cphipval  24752  lmmbr  24767  lmmbr2  24768  iscfil3  24782  iscau2  24786  cfilres  24805  bcthlem1  24833  bcthlem4  24836  bcthlem5  24837  rrxmet  24917  ioombl  25074  iccvolcl  25076  ioovolcl  25079  mbfi1fseqlem3  25227  mbfi1fseqlem4  25228  mbfi1fseqlem5  25229  ig1pcl  25685  ig1prsp  25687  aannenlem1  25833  taylplem1  25867  dvtaylp  25874  relogeftb  26085  logdivlt  26121  cxpexp  26168  rpcxpcl  26176  isppw2  26609  vmappw  26610  lgslem4  26793  lgscllem  26797  lgsneg1  26815  lgsne0  26828  nosepdm  27177  ssltdisj  27312  mulscutlem  27577  brbtwn2  28153  ax5seglem1  28176  ax5seglem2  28177  axcontlem4  28215  ewlkprop  28850  uspgr2wlkeq  28893  uhgrwkspthlem2  29001  clwlkclwwlkfo  29252  eupth2lem3lem7  29477  frgr3vlem2  29517  3cyclfrgrrn1  29528  4cycl2vnunb  29533  frgrncvvdeqlem8  29549  grpoidinvlem3  29747  isvciOLD  29821  nmcvcn  29936  ipval2lem2  29945  sspimsval  29979  isblo2  30024  nmoo0  30032  blocni  30046  isph  30063  hvadd4  30277  hiassdi  30332  ocsh  30524  chj4  30776  spansncol  30809  pjjsi  30941  hoscl  30986  hodcl  30988  hoadd4  31025  homco1  31042  homulass  31043  hoadddi  31044  hoadddir  31045  unoplin  31161  adjvalval  31178  hmoplin  31183  bralnfn  31189  brafnmul  31192  lnopmi  31241  lnopcoi  31244  hmops  31261  hmopm  31262  nmophmi  31272  lnfncnbd  31298  cnlnadjlem2  31309  adjlnop  31327  adjmul  31333  adjadd  31334  branmfn  31346  kbass5  31361  kbass6  31362  leop2  31365  leopadd  31373  leopmuli  31374  pjimai  31417  atcvatlem  31626  chirredlem2  31632  mdsymlem3  31646  mdsymlem5  31648  sumdmdii  31656  sumdmdlem  31659  cdj3lem2a  31677  cdj3lem2b  31678  cdj3lem3a  31680  cdj3i  31682  nn0difffzod  32004  xreceu  32076  cshwrnid  32113  toslublem  32130  tosglblem  32132  lmodvslmhm  32190  ogrpaddltbi  32224  archiabllem1b  32326  archiabllem2c  32329  archiabl  32332  slmdvsdir  32349  slmdvsass  32350  grplsm0l  32502  pidlnzb  32529  zarcls1  32838  pstmxmet  32866  ordtconnlem1  32893  hasheuni  33072  omsf  33284  ballotlemirc  33519  signswmnd  33557  bnj1204  34012  fineqvac  34086  fisshasheq  34093  revpfxsfxrev  34095  txpconn  34212  cvmscld  34253  satfbrsuc  34346  satfrnmapom  34350  satfun  34391  elmpps  34553  dfrdg2  34756  wsuclem  34786  segconeu  34972  linecom  35111  linethru  35114  lineintmo  35118  fnemeet2  35241  fnejoin2  35243  fvineqsneq  36282  lindsadd  36470  lindsdom  36471  lindsenlbs  36472  matunitlindflem1  36473  matunitlindflem2  36474  heicant  36512  mblfinlem1  36514  mblfinlem3  36516  ismblfin  36518  cnambfre  36525  itg2addnclem2  36529  ftc1anclem1  36550  ftc1anclem5  36554  ftc1anclem6  36555  ftc2nc  36559  areacirclem2  36566  areacirclem4  36568  areacirclem5  36569  areacirc  36570  fzmul  36598  subspopn  36609  isbndx  36639  isbnd2  36640  isbnd3  36641  ssbnd  36645  prdstotbnd  36651  heibor1  36667  rrnmet  36686  rngonegmn1l  36798  rngohomco  36831  rngoisocnv  36838  rngoisoco  36839  crngohomfo  36863  isidlc  36872  rngoidl  36881  prnc  36924  ispridlc  36927  cvrval2  38133  glbconxN  38238  hlrelat5N  38261  cvratlem  38281  cvrat2  38289  athgt  38316  3dim2  38328  llnn0  38376  lplnn0N  38407  lvoln0N  38451  snatpsubN  38610  paddasslem18  38697  pmod1i  38708  lhpexle2  38870  lhpexle3lem  38871  lhpexle3  38872  ldilcnv  38975  trlcnv  39025  trlnidatb  39037  cdleme32snaw  39295  cdleme32fvaw  39299  cdleme42ke  39345  cdlemeg46gf  39393  cdleme50trn12  39412  cdlemg1cex  39448  cdlemb3  39466  tgrpgrplem  39609  tgrpabl  39611  tendoplcl2  39638  tendo0pl  39651  tendoicl  39656  tendoipl  39657  cdlemkid3N  39793  tendoex  39835  erngdvlem4  39851  erngdvlem4-rN  39859  dib1dim  40025  dib1dim2  40028  dihglbcpreN  40160  dihmeetALTN  40187  dih1dimatlem  40189  dihatlat  40194  lcmineqlem1  40883  lcmineqlem3  40885  aks4d1p1  40930  aks4d1p7d1  40936  aks4d1p8  40941  sticksstones1  40951  sticksstones2  40952  sticksstones3  40953  sticksstones8  40958  sticksstones10  40960  sticksstones11  40961  sticksstones12a  40962  sticksstones12  40963  sticksstones17  40968  sticksstones19  40970  metakunt29  41002  metakunt30  41003  metakunt31  41004  factwoffsmonot  41012  oddcomabszz  41669  acongtr  41703  rpnnen3lem  41756  islssfg  41798  lmhmfgsplit  41814  unxpwdom3  41823  hbtlem7  41853  iocmbl  41948  ss2iundf  42396  ismnu  43006  grumnudlem  43030  ismnushort  43046  nzss  43062  dvconstbi  43079  bccbc  43090  uzmptshftfval  43091  iccdifprioo  44216  climisp  44449  limsupresxr  44469  liminfresxr  44470  dvnmul  44646  volico  44686  volioore  44693  fourierdlem74  44883  fourierdlem75  44884  sge0iunmptlemfi  45116  sge0iunmptlemre  45118  sge0iunmpt  45121  sge0xp  45132  hspmbllem2  45330  smflimlem3  45476  smfsupmpt  45518  smfinflem  45520  smfinfmpt  45522  smflimsupmpt  45532  smfliminfmpt  45535  funressnbrafv2  45939  uniimaelsetpreimafv  46051  imasetpreimafvbijlemfv1  46058  imasetpreimafvbijlemfo  46060  sprsymrelfo  46152  nnsum4primesodd  46451  nnsum4primesoddALTV  46452  nn0mnd  46576  cntzsubrng  46731  rngqiprngimfo  46767  rnghmsubcsetclem2  46828  rhmsubcsetclem2  46874  rhmsubcrngclem2  46880  lcoss  47071  snlindsntorlem  47105  mreclat  47576  aacllem  47802