![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > pm2.21dd | Structured version Visualization version GIF version |
Description: A contradiction implies anything. Deduction from pm2.21 121. (Contributed by Mario Carneiro, 9-Feb-2017.) (Proof shortened by Wolf Lammen, 22-Jul-2019.) |
Ref | Expression |
---|---|
pm2.21dd.1 | ⊢ (𝜑 → 𝜓) |
pm2.21dd.2 | ⊢ (𝜑 → ¬ 𝜓) |
Ref | Expression |
---|---|
pm2.21dd | ⊢ (𝜑 → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm2.21dd.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | pm2.21dd.2 | . . 3 ⊢ (𝜑 → ¬ 𝜓) | |
3 | 1, 2 | pm2.65i 186 | . 2 ⊢ ¬ 𝜑 |
4 | 3 | pm2.21i 117 | 1 ⊢ (𝜑 → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem is referenced by: pm2.21fal 1679 pm2.21ddne 3083 smo11 7732 ackbij1lem16 9379 cfsmolem 9414 domtriomlem 9586 konigthlem 9712 grur1 9964 uzdisj 12714 nn0disj 12757 psgnunilem2 18273 nmoleub2lem3 23291 i1f0 23860 itg2const2 23914 bposlem3 25431 bposlem9 25437 pntpbnd1 25695 fzto1st1 30393 esumpcvgval 30681 sgnmul 31146 sgnmulsgn 31153 sgnmulsgp 31154 signstfvneq0 31193 derangsn 31694 heiborlem8 34154 lkrpssN 35233 cdleme27a 36437 pellfundex 38289 monotoddzzfi 38345 jm2.23 38401 rp-isfinite6 38700 iccpartiltu 42240 iccpartigtl 42241 |
Copyright terms: Public domain | W3C validator |