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  5183  nnsucuniel  6772  nnawordex  6806  swoord2  6841  difinfsnlem  7446  exmidomni  7489  elni2  7688  cauappcvgprlemdisj  8025  caucvgprlemdisj  8048  caucvgprprlemdisj  8076  caucvgsr  8176  lelttr  8421  nnsub  9353  nn0ge2m1nn  9639  elnnz  9666  elnn0z  9669  indstr  10010  indstr2  10026  xrltnsym  10213  xrlttr  10215  xrltso  10216  xrlelttr  10226  xltnegi  10255  xsubge0  10301  ixxdisj  10323  icodisj  10412  fzm1  10525  qbtwnxr  10710  frec2uzlt2d  10863  nn0ltexp2  11170  facdiv  11199  resqrexlemgt0  11809  climuni  12085  fsumcl2lem  12191  dvdsle  12637  prmdvdsexpr  12955  prmfac1  12957  sqrt2irr  12967  phibndlem  13024  dvdsprmpweqle  13146  prmlem1  13252  prmlem2  13264  isxmet2d  15586  bpos1  16322  lgsdir2lem2  16365  lgseisenlem2  16407  wlkv0  16827  trilpolemres  17310