Theorem 3expa 1104

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 1103	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp31 243	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 97   ∧ w3a 885

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110  df-3an 887

This theorem is referenced by:  3anidm23  1194  mp3an2  1220  mpd3an3  1233  rgen3  2406  moi2  2722  sbc3ie  2831  preq12bg  3544  issod  4056  wepo  4096  reuhypd  4203  funimass4  5224  fvtp1g  5369  f1imass  5413  fcof1o  5429  f1ofveu  5500  f1ocnvfv3  5501  acexmid  5511  2ndrn  5809  rdgon  5973  frecrdg  5992  findcard  6345  findcard2  6346  findcard2s  6347  ltapig  6436  ltanqi  6500  ltmnqi  6501  lt2addnq  6502  lt2mulnq  6503  prarloclemcalc  6600  genpassl  6622  genpassu  6623  prmuloc  6664  ltexprlemm  6698  ltexprlemfl  6707  ltexprlemfu  6709  lteupri  6715  ltaprg  6717  mul4  7145  add4  7172  cnegexlem2  7187  cnegexlem3  7188  2addsub  7225  addsubeq4  7226  muladd  7381  ltleadd  7441  reapmul1  7586  apreim  7594  receuap  7650  p1le  7815  lemul12b  7827  zdiv  8328  fzind  8353  fnn0ind  8354  uzss  8493  qmulcl  8572  qreccl  8576  xrlttr  8716  icc0r  8795  iooshf  8821  elfz5  8882  elfz0fzfz0  8983  fzind2  9095  expnegap0  9263  expineg2  9264  mulexpzap  9295  expsubap  9302  expnbnd  9372  crim  9458  climshftlemg  9823