![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > pm2.18d | Structured version Visualization version Unicode version |
Description: Deduction based on reductio ad absurdum. (Contributed by FL, 12-Jul-2009.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
Ref | Expression |
---|---|
pm2.18d.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
pm2.18d |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm2.18d.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | pm2.18 114 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 17 |
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: notnot2 116 pm2.61d 162 pm2.18da 445 oplem1 975 axc11n 2143 axc11nALT 2144 weniso 6245 infssuni 7865 ordtypelem10 8042 oismo 8055 rankval3b 8297 grur1 9245 sqeqd 13229 hausflimi 20995 minveclem4 22374 minveclem4OLD 22386 ovolunnul 22453 vitali 22571 itg2mono 22711 pilem3 23409 pilem3OLD 23410 frgrancvvdeqlemB 25766 minvecolem4 26522 minvecolem4OLD 26532 bj-axc11nv 31348 contrd 32333 |
Copyright terms: Public domain | W3C validator |