Theorem pm2.01d 192

Description: Deduction based on reductio ad absurdum. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 5-Mar-2013.)

Hypothesis

Ref	Expression
pm2.01d.1	⊢ (𝜑 → (𝜓 → ¬ 𝜓))

Assertion

Ref	Expression
pm2.01d	⊢ (𝜑 → ¬ 𝜓)

Proof of Theorem pm2.01d

Step	Hyp	Ref	Expression
1		pm2.01d.1	. 2 ⊢ (𝜑 → (𝜓 → ¬ 𝜓))
2		id 23	. 2 ⊢ (¬ 𝜓 → ¬ 𝜓)
3	1, 2	pm2.61d1 182	1 ⊢ (𝜑 → ¬ 𝜓)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  pm2.65d  199  pm2.01da  811  swopo  5574  onssneli  6475  oalimcl  8547  elirrv  9569  rankcf  10786  prlem934  11042  supsrlem  11120  rpnnen1lem5  13031  rennim  15326  smu01lem  16575  opsrtoslem2  22272  cfinufil  24154  alexsub  24271  ostth3  27874  4cyclusnfrgr  30772  cvnref  32772  pconnconn  35810  untelirr  36287  dfon2lem4  36363  heiborlem10  38570  mod2addne  48258  pgnioedg1  49024  pgnioedg2  49025  pgnioedg3  49026  pgnioedg4  49027  pgnioedg5  49028  lindslinindsimp1  49387