Theorem expcomd 1462

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  1464  2moswapdc  2145  indifdir  3430  reupick  3458  issod  4370  poxp  6325  smores2  6387  smoiun  6394  mapxpen  6952  f1dmvrnfibi  7053  recexprlemm  7744  ltleletr  8161  fzind  9495  iccid  10054  ssfzo12bi  10361  dvdsabseq  12202  divalgb  12280  cncongr1  12469  difsqpwdvds  12705  lss1d  14189  txlm  14795  blsscls2  15009  metcnpi3  15033