**Description:** A syllogism inference. (Contributed by NM, 22-Aug-1995) (Proof
shortened by Wolf Lammen, 26-Jun-2022)

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

Hypotheses | syl3an2.1 | $${\u22a2}{\phi}\to {\chi}$$ | |

syl3an2.2 | $${\u22a2}\left({\psi}\wedge {\chi}\wedge {\theta}\right)\to {\tau}$$ | ||

Assertion | syl3an2 | $${\u22a2}\left({\psi}\wedge {\phi}\wedge {\theta}\right)\to {\tau}$$ |

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

1 | syl3an2.1 | $${\u22a2}{\phi}\to {\chi}$$ | |

2 | syl3an2.2 | $${\u22a2}\left({\psi}\wedge {\chi}\wedge {\theta}\right)\to {\tau}$$ | |

3 | 1 | 3anim2i | $${\u22a2}\left({\psi}\wedge {\phi}\wedge {\theta}\right)\to \left({\psi}\wedge {\chi}\wedge {\theta}\right)$$ |

4 | 3 2 | syl | $${\u22a2}\left({\psi}\wedge {\phi}\wedge {\theta}\right)\to {\tau}$$ |