Theorem pm2.01d 189

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 180	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  195  pm2.01da  795  swopo  5505  onssneli  6361  oalimcl  8353  rankcf  10464  prlem934  10720  supsrlem  10798  rpnnen1lem5  12650  rennim  14878  smu01lem  16120  opsrtoslem2  21173  cfinufil  22987  alexsub  23104  ostth3  26691  4cyclusnfrgr  28557  cvnref  30554  pconnconn  33093  untelirr  33549  dfon2lem4  33668  heiborlem10  35905  lindslinindsimp1  45686