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  5570  onssneli  6479  oalimcl  8561  elirrv  9584  rankcf  10855  prlem934  11111  supsrlem  11189  rpnnen1lem5  13102  rennim  15399  smu01lem  16648  opsrtoslem2  22358  cfinufil  24240  alexsub  24357  ostth3  27958  4cyclusnfrgr  30886  cvnref  32886  pconnconn  35975  untelirr  36452  dfon2lem4  36528  heiborlem10  38734  mod2addne  48409  pgnioedg1  49175  pgnioedg2  49176  pgnioedg3  49177  pgnioedg4  49178  pgnioedg5  49179  lindslinindsimp1  49538