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  5551  onssneli  6442  oalimcl  8497  rankcf  10700  prlem934  10956  supsrlem  11034  rpnnen1lem5  12906  rennim  15174  smu01lem  16424  opsrtoslem2  22023  cfinufil  23884  alexsub  24001  ostth3  27617  4cyclusnfrgr  30379  cvnref  32378  pconnconn  35444  untelirr  35921  dfon2lem4  35997  heiborlem10  38068  mod2addne  47721  pgnioedg1  48465  pgnioedg2  48466  pgnioedg3  48467  pgnioedg4  48468  pgnioedg5  48469  lindslinindsimp1  48814