Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > pm2.21dd | Structured version Visualization version Unicode version |
Description: A contradiction implies anything. Deduction from pm2.21 120. (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 185 | . 2 |
4 | 3 | pm2.21i 116 | 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 1505 pm2.21ddne 2878 smo11 7461 ackbij1lem16 9057 cfsmolem 9092 domtriomlem 9264 konigthlem 9390 grur1 9642 uzdisj 12413 nn0disj 12455 psgnunilem2 17915 nmoleub2lem3 22915 i1f0 23454 itg2const2 23508 bposlem3 25011 bposlem9 25017 pntpbnd1 25275 fzto1st1 29852 esumpcvgval 30140 sgnmul 30604 sgnmulsgn 30611 sgnmulsgp 30612 signstfvneq0 30649 derangsn 31152 heiborlem8 33617 lkrpssN 34450 cdleme27a 35655 pellfundex 37450 monotoddzzfi 37507 jm2.23 37563 rp-isfinite6 37864 iccpartiltu 41358 iccpartigtl 41359 |
Copyright terms: Public domain | W3C validator |