Theorem expcomd 1464

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  1466  2moswapdc  2148  indifdir  3440  reupick  3468  issod  4387  poxp  6348  smores2  6410  smoiun  6417  mapxpen  6977  f1dmvrnfibi  7079  recexprlemm  7779  ltleletr  8196  fzind  9530  iccid  10089  ssfzo12bi  10398  pfxccatin12lem2  11229  swrdccat  11233  dvdsabseq  12324  divalgb  12402  cncongr1  12591  difsqpwdvds  12827  lss1d  14312  txlm  14918  blsscls2  15132  metcnpi3  15156