Description: The third axiom of a system called "L" but proven to be a theorem since set.mm uses a different third axiom. This is named hirst after Holly P. Hirst and Jeffry L. Hirst. Axiom A3 of Mendelson p. 35. (Contributed by Jarvin Udandy, 7-Feb-2015) (Proof modification is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | hirstL-ax3 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm4.64 | ||
2 | pm4.66 | ||
3 | pm2.64 | ||
4 | 3 | com12 | |
5 | 2 4 | sylbi | |
6 | 1 5 | syl5bi |