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  702  2falsed  709  mtord  790  prlem1  981  eq0rdv  3538  csbprc  3539  rzal  3591  poirr2  5131  nnsucuniel  6668  nnawordex  6702  swoord2  6737  difinfsnlem  7303  exmidomni  7346  elni2  7539  cauappcvgprlemdisj  7876  caucvgprlemdisj  7899  caucvgprprlemdisj  7927  caucvgsr  8027  lelttr  8273  nnsub  9187  nn0ge2m1nn  9467  elnnz  9494  elnn0z  9497  indstr  9832  indstr2  9848  xrltnsym  10033  xrlttr  10035  xrltso  10036  xrlelttr  10046  xltnegi  10075  xsubge0  10121  ixxdisj  10143  icodisj  10232  fzm1  10340  qbtwnxr  10523  frec2uzlt2d  10672  nn0ltexp2  10977  facdiv  11006  resqrexlemgt0  11603  climuni  11876  fsumcl2lem  11982  dvdsle  12428  prmdvdsexpr  12745  prmfac1  12747  sqrt2irr  12757  phibndlem  12811  dvdsprmpweqle  12933  isxmet2d  15101  lgsdir2lem2  15787  lgseisenlem2  15829  wlkv0  16249  trilpolemres  16713