Theorem pm2.21d 622

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

This theorem is referenced by:  pm2.21dd  623  pm5.21  700  2falsed  707  mtord  788  prlem1  979  eq0rdv  3537  csbprc  3538  rzal  3590  poirr2  5127  nnsucuniel  6658  nnawordex  6692  swoord2  6727  difinfsnlem  7292  exmidomni  7335  elni2  7527  cauappcvgprlemdisj  7864  caucvgprlemdisj  7887  caucvgprprlemdisj  7915  caucvgsr  8015  lelttr  8261  nnsub  9175  nn0ge2m1nn  9455  elnnz  9482  elnn0z  9485  indstr  9820  indstr2  9836  xrltnsym  10021  xrlttr  10023  xrltso  10024  xrlelttr  10034  xltnegi  10063  xsubge0  10109  ixxdisj  10131  icodisj  10220  fzm1  10328  qbtwnxr  10510  frec2uzlt2d  10659  nn0ltexp2  10964  facdiv  10993  resqrexlemgt0  11574  climuni  11847  fsumcl2lem  11952  dvdsle  12398  prmdvdsexpr  12715  prmfac1  12717  sqrt2irr  12727  phibndlem  12781  dvdsprmpweqle  12903  isxmet2d  15065  lgsdir2lem2  15751  lgseisenlem2  15793  wlkv0  16180  trilpolemres  16596