Theorem expcomd 1452

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  1454  2moswapdc  2128  indifdir  3406  reupick  3434  issod  4334  poxp  6252  smores2  6314  smoiun  6321  mapxpen  6867  f1dmvrnfibi  6963  recexprlemm  7643  ltleletr  8059  fzind  9388  iccid  9945  ssfzo12bi  10245  dvdsabseq  11873  divalgb  11950  cncongr1  12123  difsqpwdvds  12357  lss1d  13667  txlm  14183  blsscls2  14397  metcnpi3  14421