**Description:** More general version of 3imtr3i . Useful for converting definitions
in a formula. (Contributed by NM, 20-May-1996) (Proof shortened by Wolf Lammen, 20-Dec-2013)

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

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

3imtr3g.2 | $${\u22a2}{\psi}\leftrightarrow {\theta}$$ | ||

3imtr3g.3 | $${\u22a2}{\chi}\leftrightarrow {\tau}$$ | ||

Assertion | 3imtr3g | $${\u22a2}{\phi}\to \left({\theta}\to {\tau}\right)$$ |

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

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

2 | 3imtr3g.2 | $${\u22a2}{\psi}\leftrightarrow {\theta}$$ | |

3 | 3imtr3g.3 | $${\u22a2}{\chi}\leftrightarrow {\tau}$$ | |

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

5 | 4 3 | syl6ib | $${\u22a2}{\phi}\to \left({\theta}\to {\tau}\right)$$ |