Metamath Proof Explorer

Theorem frege56a

Description: Proposition 56 of Frege1879 p. 50. (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)

Ref Expression
Assertion frege56a ⊢ φ ↔ ψ → if- φ χ θ → if- ψ χ θ → ψ ↔ φ → if- φ χ θ → if- ψ χ θ

Proof

Step Hyp Ref Expression
1 frege55cor1a ⊢ ψ ↔ φ → φ ↔ ψ
2 frege9 ⊢ ψ ↔ φ → φ ↔ ψ → φ ↔ ψ → if- φ χ θ → if- ψ χ θ → ψ ↔ φ → if- φ χ θ → if- ψ χ θ
3 1 2 ax-mp ⊢ φ ↔ ψ → if- φ χ θ → if- ψ χ θ → ψ ↔ φ → if- φ χ θ → if- ψ χ θ