**Description:** A negated syllogism inference. (Contributed by Wolf Lammen, 20-May-2024)

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

Hypotheses | nsyl4.1 | $${\u22a2}{\phi}\to {\psi}$$ | |

nsyl4.2 | $${\u22a2}\neg {\phi}\to {\chi}$$ | ||

Assertion | nsyl5 | $${\u22a2}\neg {\psi}\to {\chi}$$ |

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

1 | nsyl4.1 | $${\u22a2}{\phi}\to {\psi}$$ | |

2 | nsyl4.2 | $${\u22a2}\neg {\phi}\to {\chi}$$ | |

3 | 1 2 | nsyl4 | $${\u22a2}\neg {\chi}\to {\psi}$$ |

4 | 3 | con1i | $${\u22a2}\neg {\psi}\to {\chi}$$ |