![]() |
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 123. (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 193 | . 2 ⊢ ¬ 𝜑 |
4 | 3 | pm2.21i 119 | 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 1555 pm2.21ddne 3023 smo11 8391 ackbij1lem16 10266 cfsmolem 10301 domtriomlem 10473 konigthlem 10599 grur1 10851 uzdisj 13614 nn0disj 13657 psgnunilem2 19457 nmoleub2lem3 25062 i1f0 25636 itg2const2 25691 bposlem3 27239 bposlem9 27245 pntpbnd1 27539 ccatf1 32693 fzto1st1 32844 cycpmco2lem5 32872 mxidlirred 33210 rprmdvdspow 33272 esumpcvgval 33730 sgnmul 34195 sgnmulsgn 34202 sgnmulsgp 34203 signstfvneq0 34237 derangsn 34813 heiborlem8 37324 lkrpssN 38667 cdleme27a 39872 aks4d1p3 41581 aks4d1p5 41583 aks4d1p8 41590 primrootlekpowne0 41608 primrootspoweq0 41609 sticksstones22 41672 aks6d1c6lem3 41676 aks6d1c6lem4 41677 aks6d1c7lem2 41685 infdesc 42098 pellfundex 42337 monotoddzzfi 42394 jm2.23 42448 rp-isfinite6 42979 r1rankcld 43699 iccpartiltu 46791 iccpartigtl 46792 |
Copyright terms: Public domain | W3C validator |