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

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

Assertion | syl31anc | $${\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 | syl31anc.5 | $${\u22a2}\left(\left({\psi}\wedge {\chi}\wedge {\theta}\right)\wedge {\tau}\right)\to {\eta}$$ | |

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

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