Theorem pm2.01d 191

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 181	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  198  pm2.01da  808  swopo  5562  onssneli  6458  oalimcl  8523  elirrv  9539  rankcf  10729  prlem934  10985  supsrlem  11063  rpnnen1lem5  12976  rennim  15257  smu01lem  16510  opsrtoslem2  22097  cfinufil  23976  alexsub  24093  ostth3  27690  4cyclusnfrgr  30451  cvnref  32451  pconnconn  35542  untelirr  36019  dfon2lem4  36095  heiborlem10  38280  mod2addne  47925  pgnioedg1  48691  pgnioedg2  48692  pgnioedg3  48693  pgnioedg4  48694  pgnioedg5  48695  lindslinindsimp1  49040