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 190. (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 413 | . 2 ⊢ (𝜑 → (𝜓 → ¬ 𝜓)) |
3 | 2 | pm2.01d 191 | 1 ⊢ (𝜑 → ¬ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 396 |
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 208 df-an 397 |
This theorem is referenced by: efrirr 5529 omlimcl 8193 hartogslem1 8994 cfslb2n 9678 fin23lem41 9762 tskuni 10193 4sqlem18 16286 ramlb 16343 ivthlem2 23980 ivthlem3 23981 cosne0 25041 footne 26436 nsnlplig 28185 unbdqndv1 33744 unbdqndv2 33747 knoppndv 33770 fmtno4prm 43614 |
Copyright terms: Public domain | W3C validator |