Description: A closed form of syllogism (see syl ). Theorem *2.05 of WhiteheadRussell p. 100. Copy of imim2 with a different proof. (Contributed by Wolf Lammen, 17-Dec-2018) (New usage is discouraged.) (Proof modification is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | wl-luk-imim2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-luk1 | |
|
2 | 1 | wl-luk-com12 | |