| 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 418 | . 2 ⊢ (𝜑 → (𝜓 → ¬ 𝜓)) |
| 3 | 2 | pm2.01d 192 | 1 ⊢ (𝜑 → ¬ 𝜓) |
| Colors of variables: wff setvar class |
| This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 401 |
| This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
| This proof depends on definitions: df-bi 210 df-an 402 |
| This theorem is used by: efrirr 5643 omlimcl 8569 hartogslem1 9511 cfslb2n 10267 fin23lem41 10351 tskuni 10783 4sqlem18 17044 ramlb 17101 ivthlem2 25662 ivthlem3 25663 cosne0 26745 footne 29054 nsnlplig 30904 unbdqndv1 37154 unbdqndv2 37157 knoppndv 37180 dvrelog2b 42891 sticksstones22 42993 fmtno4prm 48385 |
| Copyright terms: Public domain | W3C validator |