Metamath Proof Explorer


Theorem frege61b

Description: Lemma for frege65b . Proposition 61 of Frege1879 p. 52. (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)

Ref Expression
Assertion frege61b x y φ ψ y φ ψ

Proof

Step Hyp Ref Expression
1 ax-frege58b y φ x y φ
2 frege9 y φ x y φ x y φ ψ y φ ψ
3 1 2 ax-mp x y φ ψ y φ ψ