**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}$$ | ||

syl23anc.5 | $${\u22a2}{\phi}\to {\eta}$$ | ||

syl122anc.6 | $${\u22a2}\left({\psi}\wedge \left({\chi}\wedge {\theta}\right)\wedge \left({\tau}\wedge {\eta}\right)\right)\to {\zeta}$$ | ||

Assertion | syl122anc | $${\u22a2}{\phi}\to {\zeta}$$ |

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 | syl23anc.5 | $${\u22a2}{\phi}\to {\eta}$$ | |

6 | syl122anc.6 | $${\u22a2}\left({\psi}\wedge \left({\chi}\wedge {\theta}\right)\wedge \left({\tau}\wedge {\eta}\right)\right)\to {\zeta}$$ | |

7 | 4 5 | jca | $${\u22a2}{\phi}\to \left({\tau}\wedge {\eta}\right)$$ |

8 | 1 2 3 7 6 | syl121anc | $${\u22a2}{\phi}\to {\zeta}$$ |