Metamath Proof Explorer


Theorem frege65a

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, 17-Apr-2020) (Proof modification is discouraged.)

Ref Expression
Assertion frege65a ψ χ τ η χ θ η ζ if- φ ψ τ if- φ θ ζ

Proof

Step Hyp Ref Expression
1 ifpimim if- φ ψ χ τ η if- φ ψ τ if- φ χ η
2 frege64a if- φ ψ τ if- φ χ η χ θ η ζ if- φ ψ τ if- φ θ ζ
3 1 2 syl if- φ ψ χ τ η χ θ η ζ if- φ ψ τ if- φ θ ζ
4 frege61a if- φ ψ χ τ η χ θ η ζ if- φ ψ τ if- φ θ ζ ψ χ τ η χ θ η ζ if- φ ψ τ if- φ θ ζ
5 3 4 ax-mp ψ χ τ η χ θ η ζ if- φ ψ τ if- φ θ ζ