Theorem pm2.21d 624

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

This theorem is referenced by:  pm2.21dd  625  pm5.21  703  2falsed  710  mtord  791  prlem1  982  eq0rdv  3555  csbprc  3556  rzal  3609  poirr2  5157  nnsucuniel  6730  nnawordex  6764  swoord2  6799  difinfsnlem  7392  exmidomni  7435  elni2  7634  cauappcvgprlemdisj  7971  caucvgprlemdisj  7994  caucvgprprlemdisj  8022  caucvgsr  8122  lelttr  8367  nnsub  9281  nn0ge2m1nn  9565  elnnz  9592  elnn0z  9595  indstr  9931  indstr2  9947  xrltnsym  10132  xrlttr  10134  xrltso  10135  xrlelttr  10145  xltnegi  10174  xsubge0  10220  ixxdisj  10242  icodisj  10331  fzm1  10441  qbtwnxr  10624  frec2uzlt2d  10773  nn0ltexp2  11079  facdiv  11108  resqrexlemgt0  11713  climuni  11986  fsumcl2lem  12092  dvdsle  12538  prmdvdsexpr  12855  prmfac1  12857  sqrt2irr  12867  phibndlem  12921  dvdsprmpweqle  13043  isxmet2d  15262  lgsdir2lem2  15951  lgseisenlem2  15993  wlkv0  16413  trilpolemres  16875