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

Theorem syl321anc 1340
 Description: Syllogism combined with contraction. (Contributed by NM, 11-Jul-2012.)
Hypotheses
Ref Expression
syl12anc.1 (𝜑𝜓)
syl12anc.2 (𝜑𝜒)
syl12anc.3 (𝜑𝜃)
syl22anc.4 (𝜑𝜏)
syl23anc.5 (𝜑𝜂)
syl33anc.6 (𝜑𝜁)
syl321anc.7 (((𝜓𝜒𝜃) ∧ (𝜏𝜂) ∧ 𝜁) → 𝜎)
Assertion
Ref Expression
syl321anc (𝜑𝜎)

Proof of Theorem syl321anc
StepHypRef Expression
1 syl12anc.1 . 2 (𝜑𝜓)
2 syl12anc.2 . 2 (𝜑𝜒)
3 syl12anc.3 . 2 (𝜑𝜃)
4 syl22anc.4 . . 3 (𝜑𝜏)
5 syl23anc.5 . . 3 (𝜑𝜂)
64, 5jca 553 . 2 (𝜑 → (𝜏𝜂))
7 syl33anc.6 . 2 (𝜑𝜁)
8 syl321anc.7 . 2 (((𝜓𝜒𝜃) ∧ (𝜏𝜂) ∧ 𝜁) → 𝜎)
91, 2, 3, 6, 7, 8syl311anc 1332 1 (𝜑𝜎)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031 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 196  df-an 385  df-3an 1033 This theorem is referenced by:  syl322anc  1346  cxple2ad  24271  chordthmlem3  24361  4noncolr2  33758  4noncolr1  33759  3atlem5  33791  2lplnj  33924  llnmod2i2  34167  dalawlem11  34185  dalawlem12  34186  cdleme43dN  34798  cdleme4gfv  34813  cdlemeg46nlpq  34823  cdlemg17bq  34979  cdlemg31b0N  35000  cdlemg31b0a  35001  cdlemg31c  35005  cdlemg39  35022  cdlemk47  35255  lincext3  42039
 Copyright terms: Public domain W3C validator