![]() |
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 411 | . 2 ⊢ (𝜑 → (𝜓 → ¬ 𝜓)) |
3 | 2 | pm2.01d 189 | 1 ⊢ (𝜑 → ¬ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 394 |
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 206 df-an 395 |
This theorem is referenced by: efrirr 5656 omlimcl 8580 hartogslem1 9539 cfslb2n 10265 fin23lem41 10349 tskuni 10780 4sqlem18 16899 ramlb 16956 ivthlem2 25201 ivthlem3 25202 cosne0 26274 footne 28241 nsnlplig 30001 unbdqndv1 35687 unbdqndv2 35690 knoppndv 35713 dvrelog2b 41237 sticksstones22 41290 fmtno4prm 46541 |
Copyright terms: Public domain | W3C validator |