![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > pm2.01da | Structured version Visualization version GIF version |
Description: Deduction based on reductio ad absurdum. See pm2.01 188. (Contributed by Mario Carneiro, 9-Feb-2017.) |
Ref | Expression |
---|---|
pm2.01da.1 | ⊢ ((𝜑 ∧ 𝜓) → ¬ 𝜓) |
Ref | Expression |
---|---|
pm2.01da | ⊢ (𝜑 → ¬ 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm2.01da.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → ¬ 𝜓) | |
2 | 1 | ex 412 | . 2 ⊢ (𝜑 → (𝜓 → ¬ 𝜓)) |
3 | 2 | pm2.01d 190 | 1 ⊢ (𝜑 → ¬ 𝜓) |
Colors of variables: wff setvar class |
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 5668 omlimcl 8614 hartogslem1 9579 cfslb2n 10305 fin23lem41 10389 tskuni 10820 4sqlem18 16995 ramlb 17052 ivthlem2 25500 ivthlem3 25501 cosne0 26585 footne 28745 nsnlplig 30509 unbdqndv1 36490 unbdqndv2 36493 knoppndv 36516 dvrelog2b 42047 sticksstones22 42149 fmtno4prm 47499 |
Copyright terms: Public domain | W3C validator |