**Description:** Deduction combining antecedents and consequents. Deduction associated
with imim12 and imim12i . (Contributed by NM, 7-Aug-1994) (Proof
shortened by Mel L. O'Cat, 30-Oct-2011)

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

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

imim12d.2 | $${\u22a2}{\phi}\to \left({\theta}\to {\tau}\right)$$ | ||

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

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

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

2 | imim12d.2 | $${\u22a2}{\phi}\to \left({\theta}\to {\tau}\right)$$ | |

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

4 | 1 3 | syl5d | $${\u22a2}{\phi}\to \left(\left({\chi}\to {\theta}\right)\to \left({\psi}\to {\tau}\right)\right)$$ |