Theorem pm2.21d 582

Description: A contradiction implies anything. Deduction from pm2.21 580. (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 580	. 2 ⊢ (¬ 𝜓 → (𝜓 → 𝜒))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝜓 → 𝜒))

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  pm2.21dd  583  pm5.21  644  2falsed  651  mtord  730  prlem1  915  eq0rdv  3304  csbprc  3305  rzal  3355  poirr2  4767  nnsucuniel  6159  nnawordex  6188  swoord2  6223  elni2  6618  cauappcvgprlemdisj  6955  caucvgprlemdisj  6978  caucvgprprlemdisj  7006  caucvgsr  7092  lelttr  7318  nnsub  8196  nn0ge2m1nn  8467  elnnz  8494  elnn0z  8497  indstr  8814  indstr2  8829  xrltnsym  8996  xrlttr  8998  xrltso  8999  xrlelttr  9004  xltnegi  9030  ixxdisj  9054  icodisj  9142  fzm1  9245  qbtwnxr  9396  frec2uzlt2d  9538  expival  9627  facdiv  9814  resqrexlemgt0  10107  climuni  10333  dvdsle  10452  prmdvdsexpr  10736  prmfac1  10738  sqrt2irr  10748  phibndlem  10799