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  4411  poxp  6389  smores2  6451  smoiun  6458  mapxpen  7022  f1dmvrnfibi  7127  recexprlemm  7827  ltleletr  8244  fzind  9578  iccid  10138  ssfzo12bi  10448  pfxccatin12lem2  11284  swrdccat  11288  dvdsabseq  12379  divalgb  12457  cncongr1  12646  difsqpwdvds  12882  lss1d  14368  txlm  14974  blsscls2  15188  metcnpi3  15212