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  6477  genpcdl  6501  genpcuu  6502  recexap  7396  zaddcllemneg  8040  zdiv  8084  uzaddcl  8285  fz0fzelfz0  8734  fz0fzdiffz0  8737  elfzmlbp  8740  difelfzle  8742  fzo1fzo0n0  8789  ssfzo12bi  8831  expivallem  8890  expcllem  8900  expap0  8919  mulexp  8928  cjexp  9101