Metamath Proof Explorer

Theorem frege65c

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. (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)

Ref Expression
Hypothesis frege59c.a ⊢A∈B
Assertion frege65c ⊢∀xφ→ψ→∀xψ→χ→[˙A/x]˙φ→[˙A/x]˙χ

Proof

Step Hyp Ref Expression
1 frege59c.a ⊢A∈B
2 sbcim1 ⊢[˙A/x]˙φ→ψ→[˙A/x]˙φ→[˙A/x]˙ψ
3 1 frege64c ⊢[˙A/x]˙φ→[˙A/x]˙ψ→∀xψ→χ→[˙A/x]˙φ→[˙A/x]˙χ
4 2 3 syl ⊢[˙A/x]˙φ→ψ→∀xψ→χ→[˙A/x]˙φ→[˙A/x]˙χ
5 1 frege61c ⊢[˙A/x]˙φ→ψ→∀xψ→χ→[˙A/x]˙φ→[˙A/x]˙χ→∀xφ→ψ→∀xψ→χ→[˙A/x]˙φ→[˙A/x]˙χ
6 4 5 ax-mp ⊢∀xφ→ψ→∀xψ→χ→[˙A/x]˙φ→[˙A/x]˙χ