Metamath Proof Explorer

Theorem frege65b

Description: A kind of Aristotelian inference. This judgement replaces the mode of inference barbara when the minor premise has a general context. Proposition 65 of Frege1879 p. 53.

In Frege care is taken to point out that the variables in the first clauses are independent of each other and of the final term so another valid translation could be : |- ( A. x ( [ x / a ] ph -> [ x / b ] ps ) -> ( A. y ( [ y / b ] ps -> [ y / c ] ch ) -> ( [ z / a ] ph -> [ z / c ] ch ) ) ) . But that is perhaps too pedantic a translation for this exploration. (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)

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

Proof

Step Hyp Ref Expression
1 sbim ⊢ y x φ → ψ ↔ y x φ → y x ψ
2 frege64b ⊢ y x φ → y x ψ → ∀ x ψ → χ → y x φ → y x χ
3 1 2 sylbi ⊢ y x φ → ψ → ∀ x ψ → χ → y x φ → y x χ
4 frege61b ⊢ y x φ → ψ → ∀ x ψ → χ → y x φ → y x χ → ∀ x φ → ψ → ∀ x ψ → χ → y x φ → y x χ
5 3 4 ax-mp ⊢ ∀ x φ → ψ → ∀ x ψ → χ → y x φ → y x χ