Theorem expcomd 1484

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  1486  2moswapdc  2168  indifdir  3460  reupick  3488  issod  4410  poxp  6378  smores2  6440  smoiun  6447  mapxpen  7009  f1dmvrnfibi  7111  recexprlemm  7811  ltleletr  8228  fzind  9562  iccid  10121  ssfzo12bi  10431  pfxccatin12lem2  11263  swrdccat  11267  dvdsabseq  12358  divalgb  12436  cncongr1  12625  difsqpwdvds  12861  lss1d  14347  txlm  14953  blsscls2  15167  metcnpi3  15191