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  6384  smores2  6446  smoiun  6453  mapxpen  7017  f1dmvrnfibi  7119  recexprlemm  7819  ltleletr  8236  fzind  9570  iccid  10129  ssfzo12bi  10439  pfxccatin12lem2  11271  swrdccat  11275  dvdsabseq  12366  divalgb  12444  cncongr1  12633  difsqpwdvds  12869  lss1d  14355  txlm  14961  blsscls2  15175  metcnpi3  15199