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 119. (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 184 | . 2 ⊢ ¬ 𝜑 |
4 | 3 | pm2.21i 115 | 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 1496 pm2.21ddne 2866 smo11 7348 ackbij1lem16 8940 cfsmolem 8975 domtriomlem 9147 konigthlem 9269 grur1 9521 uzdisj 12282 nn0disj 12324 psgnunilem2 17738 nmoleub2lem3 22723 i1f0 23260 itg2const2 23314 bposlem3 24811 bposlem9 24817 pntpbnd1 25075 fzto1st1 29183 esumpcvgval 29467 sgnmul 29931 sgnmulsgn 29938 sgnmulsgp 29939 signstfvneq0 29975 derangsn 30406 heiborlem8 32787 lkrpssN 33468 cdleme27a 34673 pellfundex 36468 monotoddzzfi 36525 jm2.23 36581 rp-isfinite6 36883 iccpartiltu 39960 iccpartigtl 39961 |
Copyright terms: Public domain | W3C validator |