Theorem expcomd 1451

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  1453  2moswapdc  2126  indifdir  3403  reupick  3431  issod  4331  poxp  6247  smores2  6309  smoiun  6316  mapxpen  6862  f1dmvrnfibi  6957  recexprlemm  7637  ltleletr  8053  fzind  9382  iccid  9939  ssfzo12bi  10239  dvdsabseq  11867  divalgb  11944  cncongr1  12117  difsqpwdvds  12351  lss1d  13572  txlm  14075  blsscls2  14289  metcnpi3  14313