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  799  swopo  5603  onssneli  6500  oalimcl  8598  rankcf  10817  prlem934  11073  supsrlem  11151  rpnnen1lem5  13023  rennim  15278  smu01lem  16522  opsrtoslem2  22080  cfinufil  23936  alexsub  24053  ostth3  27682  4cyclusnfrgr  30311  cvnref  32310  pconnconn  35236  untelirr  35708  dfon2lem4  35787  heiborlem10  37827  lindslinindsimp1  48374