Metamath Proof Explorer


Theorem rp-7frege

Description: Distribute antecedent and add another. (Contributed by RP, 24-Dec-2019)

Ref Expression
Assertion rp-7frege φ ψ χ θ φ ψ φ χ

Proof

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