Metamath Proof Explorer


Theorem frege63b

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

Ref Expression
Assertion frege63b y x φ ψ x φ χ y x χ

Proof

Step Hyp Ref Expression
1 frege62b y x φ x φ χ y x χ
2 frege24 y x φ x φ χ y x χ y x φ ψ x φ χ y x χ
3 1 2 ax-mp y x φ ψ x φ χ y x χ