Theorem pm2.01da 799

Description: Deduction based on reductio ad absurdum. See pm2.01 188. (Contributed by Mario Carneiro, 9-Feb-2017.)

Hypothesis

Ref	Expression
pm2.01da.1	⊢ ((𝜑 ∧ 𝜓) → ¬ 𝜓)

Assertion

Ref	Expression
pm2.01da	⊢ (𝜑 → ¬ 𝜓)

Proof of Theorem pm2.01da

Step	Hyp	Ref	Expression
1		pm2.01da.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ¬ 𝜓)
2	1	ex 412	. 2 ⊢ (𝜑 → (𝜓 → ¬ 𝜓))
3	2	pm2.01d 190	1 ⊢ (𝜑 → ¬ 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  efrirr  5665  omlimcl  8616  hartogslem1  9582  cfslb2n  10308  fin23lem41  10392  tskuni  10823  4sqlem18  17000  ramlb  17057  ivthlem2  25487  ivthlem3  25488  cosne0  26571  footne  28731  nsnlplig  30500  unbdqndv1  36509  unbdqndv2  36512  knoppndv  36535  dvrelog2b  42067  sticksstones22  42169  fmtno4prm  47562