Theorem pm2.21d 619

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

This theorem is referenced by:  pm2.21dd  620  pm5.21  695  2falsed  702  mtord  783  prlem1  973  eq0rdv  3467  csbprc  3468  rzal  3520  poirr2  5021  nnsucuniel  6495  nnawordex  6529  swoord2  6564  difinfsnlem  7097  exmidomni  7139  elni2  7312  cauappcvgprlemdisj  7649  caucvgprlemdisj  7672  caucvgprprlemdisj  7700  caucvgsr  7800  lelttr  8044  nnsub  8956  nn0ge2m1nn  9234  elnnz  9261  elnn0z  9264  indstr  9591  indstr2  9607  xrltnsym  9791  xrlttr  9793  xrltso  9794  xrlelttr  9804  xltnegi  9833  xsubge0  9879  ixxdisj  9901  icodisj  9990  fzm1  10097  qbtwnxr  10255  frec2uzlt2d  10401  nn0ltexp2  10685  facdiv  10713  resqrexlemgt0  11024  climuni  11296  fsumcl2lem  11401  dvdsle  11844  prmdvdsexpr  12144  prmfac1  12146  sqrt2irr  12156  phibndlem  12210  dvdsprmpweqle  12330  isxmet2d  13741  lgsdir2lem2  14323  trilpolemres  14672