Theorem exp31 346

Description: An exportation inference. (Contributed by NM, 26-Apr-1994.)

Hypothesis

Ref	Expression
exp31.1	⊢ (((φ ∧ ψ) ∧ χ) → θ)

Assertion

Ref	Expression
exp31	⊢ (φ → (ψ → (χ → θ)))

Proof of Theorem exp31

Step	Hyp	Ref	Expression
1		exp31.1	. . 3 ⊢ (((φ ∧ ψ) ∧ χ) → θ)
2	1	ex 108	. 2 ⊢ ((φ ∧ ψ) → (χ → θ))
3	2	ex 108	1 ⊢ (φ → (ψ → (χ → θ)))

Syntax hints:   → wi 4   ∧ wa 97

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

This theorem is referenced by:  exp41  352  exp42  353  expl  360  exbiri  364  anasss  379  an31s  504  con4biddc  753  3impa  1098  exp516  1123  r19.29af2  2446  mpteqb  5204  dffo3  5257  fconstfvm  5322  fliftfun  5379  tfrlem1  5864  tfrlem9  5876  nnsucsssuc  6010  nnaordex  6036  prarloclemup  6478  genpcdl  6502  genpcuu  6503  recexap  7416  zaddcllemneg  8060  zdiv  8104  uzaddcl  8305  fz0fzelfz0  8754  fz0fzdiffz0  8757  elfzmlbp  8760  difelfzle  8762  fzo1fzo0n0  8809  ssfzo12bi  8851  expivallem  8910  expcllem  8920  expap0  8939  mulexp  8948  cjexp  9121