Theorem expcomd 1452

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

Syntax hints:   → wi 4   ∧ wa 104

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

This theorem is referenced by:  simplbi2comg  1454  2moswapdc  2135  indifdir  3420  reupick  3448  issod  4355  poxp  6299  smores2  6361  smoiun  6368  mapxpen  6918  f1dmvrnfibi  7019  recexprlemm  7710  ltleletr  8127  fzind  9460  iccid  10019  ssfzo12bi  10320  dvdsabseq  12031  divalgb  12109  cncongr1  12298  difsqpwdvds  12534  lss1d  14017  txlm  14601  blsscls2  14815  metcnpi3  14839