Theorem pm2.01d 190

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  196  pm2.01da  798  swopo  5619  onssneli  6511  oalimcl  8616  rankcf  10846  prlem934  11102  supsrlem  11180  rpnnen1lem5  13046  rennim  15288  smu01lem  16531  opsrtoslem2  22103  cfinufil  23957  alexsub  24074  ostth3  27700  4cyclusnfrgr  30324  cvnref  32323  pconnconn  35199  untelirr  35670  dfon2lem4  35750  heiborlem10  37780  lindslinindsimp1  48186