Metamath Proof Explorer


Theorem 4syl

Description: Inference chaining three syllogisms syl . (Contributed by BJ, 14-Jul-2018) The use of this theorem is marked "discouraged" because it can cause the Metamath program "MM-PA> MINIMIZE__WITH *" command to have very long run times. However, feel free to use "MM-PA> MINIMIZE__WITH 4syl / OVERRIDE" if you wish. Remember to update the "discouraged" file if it gets used. (New usage is discouraged.)

Ref Expression
Hypotheses 4syl.1 φ ψ
4syl.2 ψ χ
4syl.3 χ θ
4syl.4 θ τ
Assertion 4syl φ τ

Proof

Step Hyp Ref Expression
1 4syl.1 φ ψ
2 4syl.2 ψ χ
3 4syl.3 χ θ
4 4syl.4 θ τ
5 1 2 3 3syl φ θ
6 5 4 syl φ τ