Description: One direction of dffrege99 . Proposition 100 of Frege1879 p. 72. (Contributed by RP, 7-Jul-2020) (Proof modification is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypothesis | frege99.z | ||
Assertion | frege100 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | frege99.z | ||
2 | 1 | dffrege99 | |
3 | frege57aid | ||
4 | 2 3 | ax-mp |