Theorem expcomd 1491

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 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  simplbi2comg  1493  2moswapdc  2177  indifdir  3487  reupick  3517  issod  4464  poxp  6468  smores2  6565  smoiun  6572  mapxpen  7148  f1dmvrnfibi  7258  recexprlemm  7992  ltleletr  8408  fzind  9766  iccid  10338  ssfzo12bi  10654  pfxccatin12lem2  11518  swrdccat  11522  dvdsabseq  12632  divalgb  12710  cncongr1  12899  difsqpwdvds  13139  lss1d  14771  txlm  15432  blsscls2  15646  metcnpi3  15670  bcmono  16226  clwwlknonex2lem2  16801  lealltlt1  16873