![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > pm2.43a | Unicode version |
Description: Inference absorbing redundant antecedent. (Contributed by NM, 7-Nov-1995.) (Proof shortened by O'Cat, 28-Nov-2008.) |
Ref | Expression |
---|---|
pm2.43a.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
pm2.43a |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 20 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | pm2.43a.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | mpid 39 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() |
This theorem is referenced by: pm2.43b 48 equveli 2042 rspc 3006 intss1 4025 fvopab3ig 5762 odi 6781 nndi 6825 inf3lem2 7540 pr2ne 7845 zorn2lem7 8338 uzind2 10318 uzindOLD 10320 elfznelfzo 11147 injresinj 11155 sqlecan 11442 brfi1uzind 11670 clatlem 14494 fiinopn 16929 usgraedg4 21359 wlkdvspthlem 21560 usgrcyclnl1 21580 dvrunz 21974 afveu 27884 ssfzo12 27990 swrdccatin12lem3c 28023 3cyclfrgrarn1 28116 vdn0frgrav2 28128 vdn1frgrav2 28130 vdgn1frgrav2 28131 ee223 28444 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 8 |
Copyright terms: Public domain | W3C validator |