Theorem pm2.21d 608

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

This theorem is referenced by:  pm2.21dd  609  pm5.21  684  2falsed  691  mtord  772  prlem1  957  eq0rdv  3407  csbprc  3408  rzal  3460  poirr2  4931  nnsucuniel  6391  nnawordex  6424  swoord2  6459  difinfsnlem  6984  exmidomni  7014  elni2  7122  cauappcvgprlemdisj  7459  caucvgprlemdisj  7482  caucvgprprlemdisj  7510  caucvgsr  7610  lelttr  7852  nnsub  8759  nn0ge2m1nn  9037  elnnz  9064  elnn0z  9067  indstr  9388  indstr2  9403  xrltnsym  9579  xrlttr  9581  xrltso  9582  xrlelttr  9589  xltnegi  9618  xsubge0  9664  ixxdisj  9686  icodisj  9775  fzm1  9880  qbtwnxr  10035  frec2uzlt2d  10177  facdiv  10484  resqrexlemgt0  10792  climuni  11062  fsumcl2lem  11167  dvdsle  11542  prmdvdsexpr  11828  prmfac1  11830  sqrt2irr  11840  phibndlem  11892  isxmet2d  12517  trilpolemres  13235