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  3468  csbprc  3469  rzal  3521  poirr2  5022  nnsucuniel  6496  nnawordex  6530  swoord2  6565  difinfsnlem  7098  exmidomni  7140  elni2  7313  cauappcvgprlemdisj  7650  caucvgprlemdisj  7673  caucvgprprlemdisj  7701  caucvgsr  7801  lelttr  8046  nnsub  8958  nn0ge2m1nn  9236  elnnz  9263  elnn0z  9266  indstr  9593  indstr2  9609  xrltnsym  9793  xrlttr  9795  xrltso  9796  xrlelttr  9806  xltnegi  9835  xsubge0  9881  ixxdisj  9903  icodisj  9992  fzm1  10100  qbtwnxr  10258  frec2uzlt2d  10404  nn0ltexp2  10689  facdiv  10718  resqrexlemgt0  11029  climuni  11301  fsumcl2lem  11406  dvdsle  11850  prmdvdsexpr  12150  prmfac1  12152  sqrt2irr  12162  phibndlem  12216  dvdsprmpweqle  12336  isxmet2d  13851  lgsdir2lem2  14433  lgseisenlem2  14454  trilpolemres  14793