**Description:** Syllogism inference with commuted antecedents. (Contributed by NM, 24-May-2005)

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

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

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

Assertion | syl5com | $${\u22a2}{\phi}\to \left({\chi}\to {\theta}\right)$$ |

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

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

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

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

4 | 3 2 | sylcom | $${\u22a2}{\phi}\to \left({\chi}\to {\theta}\right)$$ |