Theorem pm2.01d 191

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 22	. 2 ⊢ (¬ 𝜓 → ¬ 𝜓)
3	1, 2	pm2.61d1 181	1 ⊢ (𝜑 → ¬ 𝜓)

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is referenced by:  pm2.65d  198  pm2.01da  805  swopo  5540  onssneli  6431  oalimcl  8489  elirrv  9506  rankcf  10695  prlem934  10951  supsrlem  11029  rpnnen1lem5  12926  rennim  15196  smu01lem  16449  opsrtoslem2  22036  cfinufil  23915  alexsub  24032  ostth3  27623  4cyclusnfrgr  30384  cvnref  32384  pconnconn  35474  untelirr  35951  dfon2lem4  36027  heiborlem10  38202  mod2addne  47847  pgnioedg1  48613  pgnioedg2  48614  pgnioedg3  48615  pgnioedg4  48616  pgnioedg5  48617  lindslinindsimp1  48962