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  3461  reupick  3489  issod  4414  poxp  6392  smores2  6455  smoiun  6462  mapxpen  7029  f1dmvrnfibi  7137  recexprlemm  7837  ltleletr  8254  fzind  9588  iccid  10153  ssfzo12bi  10463  pfxccatin12lem2  11305  swrdccat  11309  dvdsabseq  12401  divalgb  12479  cncongr1  12668  difsqpwdvds  12904  lss1d  14390  txlm  14996  blsscls2  15210  metcnpi3  15234  clwwlknonex2lem2  16247