Metamath Proof Explorer


Theorem frege4

Description: Special case of closed form of a2d . Special case of rp-frege4g . Proposition 4 of Frege1879 p. 31. (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)

Ref Expression
Assertion frege4 φ ψ χ φ ψ φ ψ χ φ χ ψ

Proof

Step Hyp Ref Expression
1 frege3 φ ψ χ φ ψ χ φ χ ψ
2 ax-frege2 φ ψ χ φ ψ χ φ χ ψ φ ψ χ φ ψ φ ψ χ φ χ ψ
3 1 2 ax-mp φ ψ χ φ ψ φ ψ χ φ χ ψ