**Description:** A syllogism inference. Commuted form of an instance of syl .
(Contributed by BJ, 25-Oct-2021)

Ref | Expression | ||
---|---|---|---|

Hypotheses | syl11.1 | $${\u22a2}{\phi}\to \left({\psi}\to {\chi}\right)$$ | |

syl11.2 | $${\u22a2}{\theta}\to {\phi}$$ | ||

Assertion | syl11 | $${\u22a2}{\psi}\to \left({\theta}\to {\chi}\right)$$ |

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

1 | syl11.1 | $${\u22a2}{\phi}\to \left({\psi}\to {\chi}\right)$$ | |

2 | syl11.2 | $${\u22a2}{\theta}\to {\phi}$$ | |

3 | 2 1 | syl | $${\u22a2}{\theta}\to \left({\psi}\to {\chi}\right)$$ |

4 | 3 | com12 | $${\u22a2}{\psi}\to \left({\theta}\to {\chi}\right)$$ |