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 ⊢ (𝜑 → (𝜓 → 𝜒))

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  pm2.21dd  629  pm5.21  707  2falsed  714  mtord  795  prlem1  986  eq0rdv  3571  csbprc  3572  rzal  3625  ifeqeqxdc  3687  poirr2  5178  nnsucuniel  6762  nnawordex  6796  swoord2  6831  difinfsnlem  7433  exmidomni  7476  elni2  7675  cauappcvgprlemdisj  8012  caucvgprlemdisj  8035  caucvgprprlemdisj  8063  caucvgsr  8163  lelttr  8408  nnsub  9326  nn0ge2m1nn  9610  elnnz  9637  elnn0z  9640  indstr  9976  indstr2  9992  xrltnsym  10178  xrlttr  10180  xrltso  10181  xrlelttr  10191  xltnegi  10220  xsubge0  10266  ixxdisj  10288  icodisj  10377  fzm1  10490  qbtwnxr  10675  frec2uzlt2d  10824  nn0ltexp2  11130  facdiv  11159  resqrexlemgt0  11769  climuni  12042  fsumcl2lem  12148  dvdsle  12594  prmdvdsexpr  12911  prmfac1  12913  sqrt2irr  12923  phibndlem  12977  dvdsprmpweqle  13099  isxmet2d  15432  lgsdir2lem2  16131  lgseisenlem2  16173  wlkv0  16593  trilpolemres  17065