![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > pm2.21i | Structured version Visualization version Unicode version |
Description: A contradiction implies anything. Inference associated with pm2.21 111. Its associated inference is pm2.24ii 137. (Contributed by NM, 16-Sep-1993.) |
Ref | Expression |
---|---|
pm2.21i.1 |
![]() ![]() ![]() |
Ref | Expression |
---|---|
pm2.21i |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm2.21i.1 |
. . 3
![]() ![]() ![]() | |
2 | 1 | a1i 11 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | con4i 135 |
1
![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem is referenced by: pm2.24ii 137 pm2.21dd 179 pm3.2ni 872 falim 1466 nfnth 1687 rex0 3737 0ss 3766 r19.2zb 3850 ral0 3865 rabsnifsb 4031 snsssn 4132 int0 4240 axnulALT 4524 axc16b 4593 dtrucor 4633 brfvopab 6355 bropopvvv 6893 bropfvvvv 6895 tfrlem16 7129 omordi 7285 nnmordi 7350 omabs 7366 omsmolem 7372 0er 7416 pssnn 7808 fiint 7866 cantnfle 8194 r1sdom 8263 alephordi 8523 axdc3lem2 8899 canthp1 9097 elnnnn0b 10938 xltnegi 11532 xmulasslem2 11593 xrinf0 11648 xrinfm0OLD 11652 elixx3g 11673 elfz2 11817 om2uzlti 12202 hashf1lem2 12660 sum0 13864 fsum2dlem 13908 prod0 14074 fprod2dlem 14111 exprmfct 14727 4sqlem18OLD 14985 4sqlem18 14991 vdwap0 15005 ram0 15059 prmlem1a 15156 prmlem2 15169 xpsfrnel2 15549 0catg 15671 alexsub 21138 0met 21459 vitali 22650 plyeq0 23244 jensen 23993 ppiublem1 24209 ppiublem2 24210 lgsdir2lem3 24332 rpvmasum 24443 usgraedgprv 25182 4cycl4dv 25474 clwwlknprop 25579 2wlkonot3v 25682 2spthonot3v 25683 frgrareggt1 25923 topnfbey 25985 isarchi 28573 sibf0 29240 sgn3da 29485 sgnnbi 29489 sgnpbi 29490 signstfvneq0 29533 bnj98 29750 sltsolem1 30628 bisym1 31150 unqsym1 31156 amosym1 31157 subsym1 31158 bj-godellob 31253 bj-axc16b 31479 bj-dtrucor 31481 poimirlem30 32034 axc5sp1 32558 areaquad 36172 fiiuncl 37465 iblempty 37939 fveqvfvv 38770 ndmaovcl 38850 sgoldbaltlem1 39025 bgoldbtbndlem1 39045 xnn0xadd0 39238 vtxdg0v 39698 wlkbProp 39819 nn0enne 40834 |
Copyright terms: Public domain | W3C validator |