Theorem expcomd 1327

Description: Deduction form of expcom 109. (Contributed by Alan Sare, 22-Jul-2012.)

Hypothesis

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

Assertion

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

Proof of Theorem expcomd

Step	Hyp	Ref	Expression
1		expcomd.1	. . 3 ⊢ (φ → ((ψ ∧ χ) → θ))
2	1	expd 245	. 2 ⊢ (φ → (ψ → (χ → θ)))
3	2	com23 72	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:  simplbi2comg  1329  2moswapdc  1987  indifdir  3187  reupick  3215  trintssm  3861  issod  4047  poxp  5794  smores2  5850  smoiun  5857  recexprlemm  6596  ltleletr  6897  fzind  8129  iccid  8564  ssfzo12bi  8851