Theorem 3expa 1205

Description: Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.)

Hypothesis

Ref	Expression
3exp.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3expa	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Proof of Theorem 3expa

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3exp 1204	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp31 256	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 980

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 982

This theorem is referenced by:  ad4ant123  1217  ad4ant124  1218  ad4ant134  1219  ad4ant234  1220  ad5ant123  1241  3anidm23  1308  mp3an2  1336  mpd3an3  1349  rgen3  2581  moi2  2941  sbc3ie  3059  preq12bg  3799  issod  4350  wepo  4390  reuhypd  4502  funimass4  5607  fvtp1g  5766  f1imass  5817  fcof1o  5832  f1ofveu  5906  f1ocnvfv3  5907  acexmid  5917  2ndrn  6236  frecrdg  6461  oawordriexmid  6523  mapxpen  6904  findcard  6944  findcard2  6945  findcard2s  6946  ltapig  7398  ltanqi  7462  ltmnqi  7463  lt2addnq  7464  lt2mulnq  7465  prarloclemcalc  7562  genpassl  7584  genpassu  7585  prmuloc  7626  ltexprlemm  7660  ltexprlemfl  7669  ltexprlemfu  7671  lteupri  7677  ltaprg  7679  mul4  8151  add4  8180  cnegexlem2  8195  cnegexlem3  8196  2addsub  8233  addsubeq4  8234  muladd  8403  ltleadd  8465  reapmul1  8614  apreim  8622  receuap  8688  p1le  8868  lemul12b  8880  lbinf  8967  zdiv  9405  fzind  9432  fnn0ind  9433  uzss  9613  qmulcl  9702  qreccl  9707  xrlttr  9861  xaddass  9935  icc0r  9992  iooshf  10018  elfz5  10083  elfz0fzfz0  10192  fzind2  10306  ioo0  10328  ico0  10330  ioc0  10331  expnegap0  10618  expineg2  10619  mulexpzap  10650  expsubap  10658  expnbnd  10734  facndiv  10810  bccmpl  10825  bcval5  10834  bcpasc  10837  crim  11002  climshftlemg  11445  2sumeq2dv  11514  hash2iun  11622  2cprodeq2dv  11711  dvdsval3  11934  dvdsnegb  11951  muldvds1  11959  muldvds2  11960  dvdscmul  11961  dvdsmulc  11962  dvds2ln  11967  divalgb  12066  ndvdssub  12071  gcddiv  12156  rpexp1i  12292  phiprmpw  12360  hashgcdeq  12377  pythagtriplem1  12403  pockthg  12495  infpnlem1  12497  4sqlem3  12528  imasaddfnlemg  12897  mndpfo  13019  grplmulf1o  13146  grplactcnv  13174  mulgnn0subcl  13205  mulgsubcl  13206  mulgdir  13224  issubg2m  13259  issubgrpd2  13260  nmzsubg  13280  eqgen  13297  ghmmulg  13326  ghmf1  13343  kerf1ghm  13344  conjghm  13346  srglmhm  13489  srgrmhm  13490  ringlghm  13557  ringrghm  13558  oppr1g  13578  dvdsrcl2  13595  crngunit  13607  subsubrng  13710  subrgugrp  13736  subsubrg  13741  islmod  13787  lmodvsdir  13808  lmodvsass  13809  lsssubg  13873  lss1d  13879  lidlsubg  13982  lidlsubcl  13983  expghmap  14095  mulgghm2  14096  innei  14331  iscnp4  14386  cnpnei  14387  cnnei  14400  cnconst  14402  ismeti  14514  isxmet2d  14516  elbl2ps  14560  elbl2  14561  xblpnfps  14566  xblpnf  14567  xblm  14585  blininf  14592  blssexps  14597  blssex  14598  blsscls2  14661  metss  14662  metrest  14674  metcn  14682  divcnap  14723  cdivcncfap  14758  lgslem4  15119  lgscllem  15123  lgsneg1  15141  lgsne0  15154