**Description:** A mixed syllogism inference from a nested implication and a
biconditional. Useful for substituting an embedded antecedent with a
definition. (Contributed by NM, 12-Jan-1993)

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

Hypotheses | syl5bi.1 | $${\u22a2}{\phi}\leftrightarrow {\psi}$$ | |

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

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

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

1 | syl5bi.1 | $${\u22a2}{\phi}\leftrightarrow {\psi}$$ | |

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

3 | 1 | biimpi | $${\u22a2}{\phi}\to {\psi}$$ |

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