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

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

Proof of Theorem syl322anc
StepHypRef Expression
1 syl3anc.1 . 2 (𝜑𝜓)
2 syl3anc.2 . 2 (𝜑𝜒)
3 syl3anc.3 . 2 (𝜑𝜃)
4 syl3Xanc.4 . 2 (𝜑𝜏)
5 syl23anc.5 . 2 (𝜑𝜂)
6 syl33anc.6 . . 3 (𝜑𝜁)
7 syl133anc.7 . . 3 (𝜑𝜎)
86, 7jca 514 . 2 (𝜑 → (𝜁𝜎))
9 syl322anc.8 . 2 (((𝜓𝜒𝜃) ∧ (𝜏𝜂) ∧ (𝜁𝜎)) → 𝜌)
101, 2, 3, 4, 5, 8, 9syl321anc 1386 1 (𝜑𝜌)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1081 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 209  df-an 399  df-3an 1083 This theorem is referenced by:  ax5seglem6  26712  ax5seg  26716  elpaddatriN  36926  paddasslem8  36950  paddasslem12  36954  paddasslem13  36955  pmodlem1  36969  osumcllem5N  37083  pexmidlem2N  37094  cdleme3h  37358  cdleme7ga  37371  cdleme20l  37445  cdleme21ct  37452  cdleme21d  37453  cdleme21e  37454  cdleme26e  37482  cdleme26eALTN  37484  cdleme26fALTN  37485  cdleme26f  37486  cdleme26f2ALTN  37487  cdleme26f2  37488  cdleme39n  37589  cdlemh2  37939  cdlemh  37940  cdlemk12  37973  cdlemk12u  37995  cdlemkfid1N  38044  congsub  39552  mzpcong  39554  jm2.18  39570  jm2.15nn0  39585  jm2.27c  39589
 Copyright terms: Public domain W3C validator