Theorem 3expa 1103

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 1102	. 2 ⊢ (φ → (ψ → (χ → θ)))
3	2	imp31 243	1 ⊢ (((φ ∧ ψ) ∧ χ) → θ)

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

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 886

This theorem is referenced by:  3anidm23  1193  mp3an2  1219  mpd3an3  1232  rgen3  2400  moi2  2716  sbc3ie  2825  preq12bg  3535  issod  4047  reuhypd  4169  funimass4  5167  fvtp1g  5312  f1imass  5356  fcof1o  5372  f1ofveu  5443  f1ocnvfv3  5444  acexmid  5454  2ndrn  5751  rdgon  5913  frecrdg  5931  ltapig  6322  ltanqi  6386  ltmnqi  6387  lt2addnq  6388  prarloclemcalc  6485  genpassl  6507  genpassu  6508  prmuloc  6547  ltexprlemm  6574  ltexprlemfl  6583  ltexprlemfu  6585  ltaprg  6592  mul4  6942  add4  6969  cnegexlem2  6984  cnegexlem3  6985  2addsub  7022  addsubeq4  7023  muladd  7177  ltleadd  7236  reapmul1  7379  apreim  7387  receuap  7432  p1le  7596  lemul12b  7608  zdiv  8104  fzind  8129  fnn0ind  8130  uzss  8269  qmulcl  8348  qreccl  8351  xrlttr  8486  icc0r  8565  iooshf  8591  elfz5  8652  elfz0fzfz0  8753  fzind2  8865  expnegap0  8917  expineg2  8918  mulexpzap  8949  expsubap  8956  expnbnd  9025  crim  9086