Theorem pm2.21d 620

Description: A contradiction implies anything. Deduction from pm2.21 618. (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 618	. 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 616

This theorem is referenced by:  pm2.21dd  621  pm5.21  696  2falsed  703  mtord  784  prlem1  975  eq0rdv  3496  csbprc  3497  rzal  3549  poirr2  5063  nnsucuniel  6562  nnawordex  6596  swoord2  6631  difinfsnlem  7174  exmidomni  7217  elni2  7398  cauappcvgprlemdisj  7735  caucvgprlemdisj  7758  caucvgprprlemdisj  7786  caucvgsr  7886  lelttr  8132  nnsub  9046  nn0ge2m1nn  9326  elnnz  9353  elnn0z  9356  indstr  9684  indstr2  9700  xrltnsym  9885  xrlttr  9887  xrltso  9888  xrlelttr  9898  xltnegi  9927  xsubge0  9973  ixxdisj  9995  icodisj  10084  fzm1  10192  qbtwnxr  10364  frec2uzlt2d  10513  nn0ltexp2  10818  facdiv  10847  resqrexlemgt0  11202  climuni  11475  fsumcl2lem  11580  dvdsle  12026  prmdvdsexpr  12343  prmfac1  12345  sqrt2irr  12355  phibndlem  12409  dvdsprmpweqle  12531  isxmet2d  14668  lgsdir2lem2  15354  lgseisenlem2  15396  trilpolemres  15773