Theorem expcomd 1400

Description: Deduction form of expcom 115. (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 256	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	com23 78	1 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃)))

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 107

This theorem is referenced by:  simplbi2comg  1402  2moswapdc  2065  indifdir  3298  reupick  3326  issod  4201  poxp  6083  smores2  6145  smoiun  6152  mapxpen  6695  f1dmvrnfibi  6784  recexprlemm  7377  ltleletr  7766  fzind  9067  iccid  9598  ssfzo12bi  9892  dvdsabseq  11390  divalgb  11467  cncongr1  11627  txlm  12287  blsscls2  12479  metcnpi3  12503