Metamath Proof Explorer
Description: Theorem *4.43 of WhiteheadRussell p. 119. (Contributed by NM, 3-Jan-2005) (Proof shortened by Wolf Lammen, 26-Nov-2012)
|
|
Ref |
Expression |
|
Assertion |
pm4.43 |
|
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
pm3.24 |
|
2 |
1
|
biorfi |
|
3 |
|
ordi |
|
4 |
2 3
|
bitri |
|