Theorem expcomd 1417

Description: Deduction form of expcom 115. (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 256	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	com23 78	1 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃)))

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  simplbi2comg  1419  2moswapdc  2089  indifdir  3332  reupick  3360  issod  4241  poxp  6129  smores2  6191  smoiun  6198  mapxpen  6742  f1dmvrnfibi  6832  recexprlemm  7432  ltleletr  7846  fzind  9166  iccid  9708  ssfzo12bi  10002  dvdsabseq  11545  divalgb  11622  cncongr1  11784  txlm  12448  blsscls2  12662  metcnpi3  12686