![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > pm2.01d | Structured version Visualization version Unicode version |
Description: Deduction based on reductio ad absurdum. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 5-Mar-2013.) |
Ref | Expression |
---|---|
pm2.01d.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
pm2.01d |
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm2.01d.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | id 22 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | pm2.61d1 164 |
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.65d 180 pm2.01da 449 swopo 4770 oalimcl 7279 rankcf 9220 prlem934 9476 supsrlem 9553 rpnnen1lem5 11317 rennim 13379 smu01lem 14538 opsrtoslem2 18785 cfinufil 21021 alexsub 21138 ostth3 24555 4cyclusnfrgra 25826 cvnref 28025 pconcon 30026 untelirr 30407 dfon2lem4 30503 heiborlem10 32216 lindslinindsimp1 40758 |
Copyright terms: Public domain | W3C validator |