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  5577  onssneli  6506  oalimcl  8606  elirrv  9628  rankcf  10901  prlem934  11157  supsrlem  11235  rpnnen1lem5  13149  rennim  15449  smu01lem  16699  opsrtoslem2  22420  cfinufil  24302  alexsub  24419  ostth3  28022  4cyclusnfrgr  30950  cvnref  32950  pconnconn  36204  mirimanofffr  36670  untelirr  36688  dfon2lem4  36763  heiborlem10  39020  mod2addne  48713  pgnioedg1  49479  pgnioedg2  49480  pgnioedg3  49481  pgnioedg4  49482  pgnioedg5  49483  lindslinindsimp1  49900