Description: Add antecedent to ax-frege2 . More general statement than frege3 . Like ax-frege2 , it is essentially a closed form of mpd , however it has an extra antecedent.
It would be more natural to prove from a1i and ax-frege2 in Metamath. (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | rp-frege3g |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-frege2 | ||
2 | ax-frege1 | ||
3 | 1 2 | ax-mp |