Theorem pm2.01d 193

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 183	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  799  swopo  5464  onssneli  6301  oalimcl  8266  rankcf  10356  prlem934  10612  supsrlem  10690  rpnnen1lem5  12542  rennim  14767  smu01lem  16007  opsrtoslem2  20967  cfinufil  22779  alexsub  22896  ostth3  26473  4cyclusnfrgr  28329  cvnref  30326  pconnconn  32860  untelirr  33316  dfon2lem4  33432  heiborlem10  35664  lindslinindsimp1  45414