**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 | $${\u22a2}{\phi}\to {\psi}$$ | |

4syl.2 | $${\u22a2}{\psi}\to {\chi}$$ | ||

4syl.3 | $${\u22a2}{\chi}\to {\theta}$$ | ||

4syl.4 | $${\u22a2}{\theta}\to {\tau}$$ | ||

Assertion | 4syl | $${\u22a2}{\phi}\to {\tau}$$ |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | 4syl.1 | $${\u22a2}{\phi}\to {\psi}$$ | |

2 | 4syl.2 | $${\u22a2}{\psi}\to {\chi}$$ | |

3 | 4syl.3 | $${\u22a2}{\chi}\to {\theta}$$ | |

4 | 4syl.4 | $${\u22a2}{\theta}\to {\tau}$$ | |

5 | 1 2 3 | 3syl | $${\u22a2}{\phi}\to {\theta}$$ |

6 | 5 4 | syl | $${\u22a2}{\phi}\to {\tau}$$ |