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

Theorem syl322anc 1396
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 510 . 2 (𝜑 → (𝜁𝜎))
9 syl322anc.8 . 2 (((𝜓𝜒𝜃) ∧ (𝜏𝜂) ∧ (𝜁𝜎)) → 𝜌)
101, 2, 3, 4, 5, 8, 9syl321anc 1390 1 (𝜑𝜌)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  w3a 1085
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 206  df-an 395  df-3an 1087
This theorem is referenced by:  cofcut2d  27648  ax5seglem6  28459  ax5seg  28463  elpaddatriN  38977  paddasslem8  39001  paddasslem12  39005  paddasslem13  39006  pmodlem1  39020  osumcllem5N  39134  pexmidlem2N  39145  cdleme3h  39409  cdleme7ga  39422  cdleme20l  39496  cdleme21ct  39503  cdleme21d  39504  cdleme21e  39505  cdleme26e  39533  cdleme26eALTN  39535  cdleme26fALTN  39536  cdleme26f  39537  cdleme26f2ALTN  39538  cdleme26f2  39539  cdleme39n  39640  cdlemh2  39990  cdlemh  39991  cdlemk12  40024  cdlemk12u  40046  cdlemkfid1N  40095  congsub  42011  mzpcong  42013  jm2.18  42029  jm2.15nn0  42044  jm2.27c  42048
  Copyright terms: Public domain W3C validator