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  3479  reupick  3507  issod  4442  poxp  6430  smores2  6527  smoiun  6534  mapxpen  7103  f1dmvrnfibi  7213  recexprlemm  7944  ltleletr  8360  fzind  9699  iccid  10264  ssfzo12bi  10577  pfxccatin12lem2  11431  swrdccat  11435  dvdsabseq  12541  divalgb  12619  cncongr1  12808  difsqpwdvds  13044  lss1d  14580  txlm  15193  blsscls2  15407  metcnpi3  15431  clwwlknonex2lem2  16482