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

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

Proof of Theorem syl321anc
StepHypRef Expression
1 syl3anc.1 . 2 (𝜑𝜓)
2 syl3anc.2 . 2 (𝜑𝜒)
3 syl3anc.3 . 2 (𝜑𝜃)
4 syl3Xanc.4 . . 3 (𝜑𝜏)
5 syl23anc.5 . . 3 (𝜑𝜂)
64, 5jca 511 . 2 (𝜑 → (𝜏𝜂))
7 syl33anc.6 . 2 (𝜑𝜁)
8 syl321anc.7 . 2 (((𝜓𝜒𝜃) ∧ (𝜏𝜂) ∧ 𝜁) → 𝜎)
91, 2, 3, 6, 7, 8syl311anc 1383 1 (𝜑𝜎)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1086
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 396  df-3an 1088
This theorem is referenced by:  syl322anc  1397  cxple2ad  26466  chordthmlem3  26572  nosupbnd1lem3  27446  nosupbnd1lem4  27447  noinfbnd1lem3  27461  noinfbnd1lem4  27462  4noncolr2  38629  4noncolr1  38630  3atlem5  38662  2lplnj  38795  llnmod2i2  39038  dalawlem11  39056  dalawlem12  39057  cdleme43dN  39667  cdleme4gfv  39682  cdlemeg46nlpq  39692  cdlemg17bq  39848  cdlemg31b0N  39869  cdlemg31b0a  39870  cdlemg31c  39874  cdlemg39  39891  cdlemk47  40124  lincext3  47226
  Copyright terms: Public domain W3C validator