Description: Theorem *3.48 of WhiteheadRussell p. 114. (Contributed by NM, 28-Jan-1997)
Ref | Expression | ||
---|---|---|---|
Assertion | pm3.48 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orc | |
|
2 | 1 | imim2i | |
3 | olc | |
|
4 | 3 | imim2i | |
5 | 2 4 | jaao | |