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  5582  onssneli  6482  oalimcl  8547  elirrv  9562  rankcf  10773  prlem934  11029  supsrlem  11107  rpnnen1lem5  13017  rennim  15310  smu01lem  16561  opsrtoslem2  22237  cfinufil  24116  alexsub  24233  ostth3  27833  4cyclusnfrgr  30690  cvnref  32690  pconnconn  35736  untelirr  36213  dfon2lem4  36289  heiborlem10  38504  mod2addne  48140  pgnioedg1  48906  pgnioedg2  48907  pgnioedg3  48908  pgnioedg4  48909  pgnioedg5  48910  lindslinindsimp1  49270