Metamath Proof Explorer

Theorem frege60b

Description: Swap antecedents of ax-frege58b . Proposition 60 of Frege1879 p. 52. (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)

Ref Expression
Assertion frege60b ⊢ ∀ x φ → ψ → χ → y x ψ → y x φ → y x χ

Proof

Step Hyp Ref Expression
1 ax-frege58b ⊢ ∀ x φ → ψ → χ → y x φ → ψ → χ
2 sbim ⊢ y x φ → ψ → χ ↔ y x φ → y x ψ → χ
3 sbim ⊢ y x ψ → χ ↔ y x ψ → y x χ
4 3 imbi2i ⊢ y x φ → y x ψ → χ ↔ y x φ → y x ψ → y x χ
5 2 4 bitri ⊢ y x φ → ψ → χ ↔ y x φ → y x ψ → y x χ
6 1 5 sylib ⊢ ∀ x φ → ψ → χ → y x φ → y x ψ → y x χ
7 frege12 ⊢ ∀ x φ → ψ → χ → y x φ → y x ψ → y x χ → ∀ x φ → ψ → χ → y x ψ → y x φ → y x χ
8 6 7 ax-mp ⊢ ∀ x φ → ψ → χ → y x ψ → y x φ → y x χ