**Description:** Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012)

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

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

syl3anc.2 | $${\u22a2}{\phi}\to {\chi}$$ | ||

syl3anc.3 | $${\u22a2}{\phi}\to {\theta}$$ | ||

syl3Xanc.4 | $${\u22a2}{\phi}\to {\tau}$$ | ||

syl121anc.5 | $${\u22a2}\left({\psi}\wedge \left({\chi}\wedge {\theta}\right)\wedge {\tau}\right)\to {\eta}$$ | ||

Assertion | syl121anc | $${\u22a2}{\phi}\to {\eta}$$ |

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

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

2 | syl3anc.2 | $${\u22a2}{\phi}\to {\chi}$$ | |

3 | syl3anc.3 | $${\u22a2}{\phi}\to {\theta}$$ | |

4 | syl3Xanc.4 | $${\u22a2}{\phi}\to {\tau}$$ | |

5 | syl121anc.5 | $${\u22a2}\left({\psi}\wedge \left({\chi}\wedge {\theta}\right)\wedge {\tau}\right)\to {\eta}$$ | |

6 | 2 3 | jca | $${\u22a2}{\phi}\to \left({\chi}\wedge {\theta}\right)$$ |

7 | 1 6 4 5 | syl3anc | $${\u22a2}{\phi}\to {\eta}$$ |