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 23	. 2 ⊢ (¬ 𝜓 → ¬ 𝜓)
3	1, 2	pm2.61d1 182	1 ⊢ (𝜑 → ¬ 𝜓)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  pm2.65d  199  pm2.01da  811  swopo  5569  onssneli  6480  oalimcl  8572  elirrv  9595  rankcf  10866  prlem934  11122  supsrlem  11200  rpnnen1lem5  13113  rennim  15412  smu01lem  16661  opsrtoslem2  22371  cfinufil  24253  alexsub  24370  ostth3  27971  4cyclusnfrgr  30899  cvnref  32899  pconnconn  36083  untelirr  36566  dfon2lem4  36641  heiborlem10  38848  mod2addne  48534  pgnioedg1  49300  pgnioedg2  49301  pgnioedg3  49302  pgnioedg4  49303  pgnioedg5  49304  lindslinindsimp1  49663