![]() |
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 414 | . 2 ⊢ (𝜑 → (𝜓 → ¬ 𝜓)) |
3 | 2 | pm2.01d 189 | 1 ⊢ (𝜑 → ¬ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 397 |
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 398 |
This theorem is referenced by: efrirr 5658 omlimcl 8578 hartogslem1 9537 cfslb2n 10263 fin23lem41 10347 tskuni 10778 4sqlem18 16895 ramlb 16952 ivthlem2 24969 ivthlem3 24970 cosne0 26038 footne 27974 nsnlplig 29734 unbdqndv1 35384 unbdqndv2 35387 knoppndv 35410 dvrelog2b 40931 sticksstones22 40984 fmtno4prm 46243 |
Copyright terms: Public domain | W3C validator |