Theorem pm2.21d 557

Description: A contradiction implies anything. Deduction from pm2.21 555. (Contributed by NM, 10-Feb-1996.)

Hypothesis

Ref	Expression
pm2.21d.1	⊢ (𝜑 → ¬ 𝜓)

Assertion

Ref	Expression
pm2.21d	⊢ (𝜑 → (𝜓 → 𝜒))

Proof of Theorem pm2.21d

Step	Hyp	Ref	Expression
1		pm2.21d.1	. 2 ⊢ (𝜑 → ¬ 𝜓)
2		pm2.21 555	. 2 ⊢ (¬ 𝜓 → (𝜓 → 𝜒))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝜓 → 𝜒))

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-in2 553

This theorem is referenced by:  pm2.21dd  558  pm5.21  619  2falsed  626  mtord  705  prlem1  889  eq0rdv  3286  csbprc  3287  rzal  3343  poirr2  4742  nnawordex  6129  swoord2  6164  elni2  6440  cauappcvgprlemdisj  6777  caucvgprlemdisj  6800  caucvgprprlemdisj  6828  caucvgsr  6914  lelttr  7135  nnsub  7998  nn0ge2m1nn  8269  elnnz  8282  elnn0z  8285  indstr  8602  indstr2  8613  xrltnsym  8785  xrlttr  8787  xrltso  8788  xrlelttr  8793  xltnegi  8819  ixxdisj  8843  icodisj  8931  fzm1  9034  frec2uzlt2d  9319  expival  9387  facdiv  9570  resqrexlemgt0  9810  climuni  10008  dvdsle  10119  sqrt2irr  10194