Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl332anc Structured version   Visualization version   GIF version

Theorem syl332anc 1354
 Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
syl12anc.1 (𝜑𝜓)
syl12anc.2 (𝜑𝜒)
syl12anc.3 (𝜑𝜃)
syl22anc.4 (𝜑𝜏)
syl23anc.5 (𝜑𝜂)
syl33anc.6 (𝜑𝜁)
syl133anc.7 (𝜑𝜎)
syl233anc.8 (𝜑𝜌)
syl332anc.9 (((𝜓𝜒𝜃) ∧ (𝜏𝜂𝜁) ∧ (𝜎𝜌)) → 𝜇)
Assertion
Ref Expression
syl332anc (𝜑𝜇)

Proof of Theorem syl332anc
StepHypRef Expression
1 syl12anc.1 . 2 (𝜑𝜓)
2 syl12anc.2 . 2 (𝜑𝜒)
3 syl12anc.3 . 2 (𝜑𝜃)
4 syl22anc.4 . 2 (𝜑𝜏)
5 syl23anc.5 . 2 (𝜑𝜂)
6 syl33anc.6 . 2 (𝜑𝜁)
7 syl133anc.7 . . 3 (𝜑𝜎)
8 syl233anc.8 . . 3 (𝜑𝜌)
97, 8jca 554 . 2 (𝜑 → (𝜎𝜌))
10 syl332anc.9 . 2 (((𝜓𝜒𝜃) ∧ (𝜏𝜂𝜁) ∧ (𝜎𝜌)) → 𝜇)
111, 2, 3, 4, 5, 6, 9, 10syl331anc 1348 1 (𝜑𝜇)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1036 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8 This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1038 This theorem is referenced by:  mdetunilem5  20341  mdetuni0  20346  lnjatN  34546  lncmp  34549  cdlema1N  34557  4atexlemex6  34840  cdlemd4  34968  cdleme18c  35060  cdleme18d  35062  cdleme19b  35072  cdleme21ct  35097  cdleme21d  35098  cdleme21e  35099  cdleme21k  35106  cdleme22g  35116  cdleme24  35120  cdleme27a  35135  cdleme27N  35137  cdleme28a  35138  cdleme40n  35236  cdlemg16zz  35428  cdlemg37  35457  cdlemk21-2N  35659  cdlemk20-2N  35660  cdlemk28-3  35676  cdlemk19xlem  35710
 Copyright terms: Public domain W3C validator