![]() |
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 7727 ackbij1lem16 9372 cfsmolem 9407 domtriomlem 9579 konigthlem 9705 grur1 9957 uzdisj 12707 nn0disj 12750 psgnunilem2 18266 nmoleub2lem3 23284 i1f0 23853 itg2const2 23907 bposlem3 25424 bposlem9 25430 pntpbnd1 25688 fzto1st1 30386 esumpcvgval 30674 sgnmul 31139 sgnmulsgn 31146 sgnmulsgp 31147 signstfvneq0 31186 derangsn 31687 heiborlem8 34152 lkrpssN 35231 cdleme27a 36435 pellfundex 38287 monotoddzzfi 38343 jm2.23 38399 rp-isfinite6 38698 iccpartiltu 42239 iccpartigtl 42240 |
Copyright terms: Public domain | W3C validator |