| 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 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 |
| Copyright terms: Public domain | W3C validator |