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 ⊢ (𝜑 → ¬ 𝜓)

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  199  pm2.01da  810  swopo  5580  onssneli  6478  oalimcl  8541  elirrv  9555  rankcf  10757  prlem934  11013  supsrlem  11091  rpnnen1lem5  13000  rennim  15286  smu01lem  16538  opsrtoslem2  22207  cfinufil  24085  alexsub  24202  ostth3  27802  4cyclusnfrgr  30643  cvnref  32643  pconnconn  35723  untelirr  36200  dfon2lem4  36276  heiborlem10  38471  mod2addne  48107  pgnioedg1  48873  pgnioedg2  48874  pgnioedg3  48875  pgnioedg4  48876  pgnioedg5  48877  lindslinindsimp1  49237