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 ⊢ φ → ψ → χ → φ → ψ → φ → ψ → χ → φ → χ → ψ