Theorem pm2.21d 628

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in2 624

This theorem is used by:  pm2.21dd  629  pm5.21  707  2falsed  714  mtord  795  prlem1  986  eq0rdv  3571  csbprc  3572  rzal  3625  ifeqeqxdc  3687  poirr2  5180  nnsucuniel  6768  nnawordex  6802  swoord2  6837  difinfsnlem  7439  exmidomni  7482  elni2  7681  cauappcvgprlemdisj  8018  caucvgprlemdisj  8041  caucvgprprlemdisj  8069  caucvgsr  8169  lelttr  8414  nnsub  9344  nn0ge2m1nn  9629  elnnz  9656  elnn0z  9659  indstr  9995  indstr2  10011  xrltnsym  10197  xrlttr  10199  xrltso  10200  xrlelttr  10210  xltnegi  10239  xsubge0  10285  ixxdisj  10307  icodisj  10396  fzm1  10509  qbtwnxr  10694  frec2uzlt2d  10843  nn0ltexp2  11149  facdiv  11178  resqrexlemgt0  11788  climuni  12061  fsumcl2lem  12167  dvdsle  12613  prmdvdsexpr  12930  prmfac1  12932  sqrt2irr  12942  phibndlem  12996  dvdsprmpweqle  13118  isxmet2d  15451  lgsdir2lem2  16160  lgseisenlem2  16202  wlkv0  16622  trilpolemres  17103