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  4466  poxp  6472  smores2  6569  smoiun  6576  mapxpen  7153  f1dmvrnfibi  7263  recexprlemm  7998  ltleletr  8414  fzind  9773  iccid  10345  ssfzo12bi  10661  pfxccatin12lem2  11526  swrdccat  11530  dvdsabseq  12640  divalgb  12718  cncongr1  12907  difsqpwdvds  13147  lss1d  14830  txlm  15517  blsscls2  15731  metcnpi3  15755  bcmono  16316  clwwlknonex2lem2  16896  lealltlt1  16968