Metamath Proof Explorer


Theorem rp-frege3g

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 φ ψ χ θ ψ χ ψ θ

Proof

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