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 22	. 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  198  pm2.01da  797  swopo  5484  onssneli  6300  oalimcl  8186  rankcf  10199  prlem934  10455  supsrlem  10533  rpnnen1lem5  12381  rennim  14598  smu01lem  15834  opsrtoslem2  20265  cfinufil  22536  alexsub  22653  ostth3  26214  4cyclusnfrgr  28071  cvnref  30068  pconnconn  32478  untelirr  32934  dfon2lem4  33031  heiborlem10  35113  lindslinindsimp1  44532