Theorem pm2.21d 609

Description: A contradiction implies anything. Deduction from pm2.21 607. (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 607	. 2 ⊢ (¬ 𝜓 → (𝜓 → 𝜒))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝜓 → 𝜒))

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  pm2.21dd  610  pm5.21  685  2falsed  692  mtord  773  prlem1  958  eq0rdv  3438  csbprc  3439  rzal  3491  poirr2  4979  nnsucuniel  6443  nnawordex  6476  swoord2  6511  difinfsnlem  7044  exmidomni  7086  elni2  7235  cauappcvgprlemdisj  7572  caucvgprlemdisj  7595  caucvgprprlemdisj  7623  caucvgsr  7723  lelttr  7966  nnsub  8873  nn0ge2m1nn  9151  elnnz  9178  elnn0z  9181  indstr  9505  indstr2  9521  xrltnsym  9701  xrlttr  9703  xrltso  9704  xrlelttr  9711  xltnegi  9740  xsubge0  9786  ixxdisj  9808  icodisj  9897  fzm1  10003  qbtwnxr  10161  frec2uzlt2d  10307  facdiv  10616  resqrexlemgt0  10924  climuni  11194  fsumcl2lem  11299  dvdsle  11740  prmdvdsexpr  12029  prmfac1  12031  sqrt2irr  12041  phibndlem  12095  isxmet2d  12790  trilpolemres  13655