Theorem expcomd 1487

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  1489  2moswapdc  2173  indifdir  3481  reupick  3509  issod  4445  poxp  6441  smores2  6538  smoiun  6545  mapxpen  7114  f1dmvrnfibi  7224  recexprlemm  7955  ltleletr  8371  fzind  9714  iccid  10280  ssfzo12bi  10595  pfxccatin12lem2  11451  swrdccat  11455  dvdsabseq  12561  divalgb  12639  cncongr1  12828  difsqpwdvds  13064  lss1d  14660  txlm  15273  blsscls2  15487  metcnpi3  15511  clwwlknonex2lem2  16562  lealltlt1  16634