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  2171  indifdir  3476  reupick  3504  issod  4439  poxp  6427  smores2  6524  smoiun  6531  mapxpen  7100  f1dmvrnfibi  7210  recexprlemm  7935  ltleletr  8351  fzind  9689  iccid  10254  ssfzo12bi  10566  pfxccatin12lem2  11416  swrdccat  11420  dvdsabseq  12526  divalgb  12604  cncongr1  12793  difsqpwdvds  13029  lss1d  14518  txlm  15131  blsscls2  15345  metcnpi3  15369  clwwlknonex2lem2  16420