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  2584  moi2  2945  sbc3ie  3063  preq12bg  3804  issod  4355  wepo  4395  reuhypd  4507  funimass4  5614  fvtp1g  5773  f1imass  5824  fcof1o  5839  f1ofveu  5913  f1ocnvfv3  5914  acexmid  5924  2ndrn  6250  frecrdg  6475  oawordriexmid  6537  mapxpen  6918  findcard  6958  findcard2  6959  findcard2s  6960  ltapig  7424  ltanqi  7488  ltmnqi  7489  lt2addnq  7490  lt2mulnq  7491  prarloclemcalc  7588  genpassl  7610  genpassu  7611  prmuloc  7652  ltexprlemm  7686  ltexprlemfl  7695  ltexprlemfu  7697  lteupri  7703  ltaprg  7705  mul4  8177  add4  8206  cnegexlem2  8221  cnegexlem3  8222  2addsub  8259  addsubeq4  8260  muladd  8429  ltleadd  8492  reapmul1  8641  apreim  8649  receuap  8715  p1le  8895  lemul12b  8907  lbinf  8994  zdiv  9433  fzind  9460  fnn0ind  9461  uzss  9641  qmulcl  9730  qreccl  9735  xrlttr  9889  xaddass  9963  icc0r  10020  iooshf  10046  elfz5  10111  elfz0fzfz0  10220  fzind2  10334  ioo0  10368  ico0  10370  ioc0  10371  expnegap0  10658  expineg2  10659  mulexpzap  10690  expsubap  10698  expnbnd  10774  facndiv  10850  bccmpl  10865  bcval5  10874  bcpasc  10877  crim  11042  climshftlemg  11486  2sumeq2dv  11555  hash2iun  11663  2cprodeq2dv  11752  dvdsval3  11975  dvdsnegb  11992  muldvds1  12000  muldvds2  12001  dvdscmul  12002  dvdsmulc  12003  dvds2ln  12008  divalgb  12109  ndvdssub  12114  gcddiv  12213  rpexp1i  12349  phiprmpw  12417  hashgcdeq  12435  pythagtriplem1  12461  pockthg  12553  infpnlem1  12555  4sqlem3  12586  imasaddfnlemg  13018  mndpfo  13142  grplmulf1o  13278  grplactcnv  13306  mulgnn0subcl  13343  mulgsubcl  13344  mulgdir  13362  issubg2m  13397  issubgrpd2  13398  nmzsubg  13418  eqgen  13435  ghmmulg  13464  ghmf1  13481  kerf1ghm  13482  conjghm  13484  srglmhm  13627  srgrmhm  13628  ringlghm  13695  ringrghm  13696  oppr1g  13716  dvdsrcl2  13733  crngunit  13745  subsubrng  13848  subrgugrp  13874  subsubrg  13879  islmod  13925  lmodvsdir  13946  lmodvsass  13947  lsssubg  14011  lss1d  14017  lidlsubg  14120  lidlsubcl  14121  expghmap  14241  mulgghm2  14242  innei  14507  iscnp4  14562  cnpnei  14563  cnnei  14576  cnconst  14578  ismeti  14690  isxmet2d  14692  elbl2ps  14736  elbl2  14737  xblpnfps  14742  xblpnf  14743  xblm  14761  blininf  14768  blssexps  14773  blssex  14774  blsscls2  14837  metss  14838  metrest  14850  metcn  14858  divcnap  14909  cdivcncfap  14948  dvply1  15109  lgslem4  15352  lgscllem  15356  lgsneg1  15374  lgsne0  15387