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

Theorem syl312anc 1390
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 (𝜑𝜁)
syl312anc.7 (((𝜓𝜒𝜃) ∧ 𝜏 ∧ (𝜂𝜁)) → 𝜎)
Assertion
Ref Expression
syl312anc (𝜑𝜎)

Proof of Theorem syl312anc
StepHypRef Expression
1 syl3anc.1 . 2 (𝜑𝜓)
2 syl3anc.2 . 2 (𝜑𝜒)
3 syl3anc.3 . 2 (𝜑𝜃)
4 syl3Xanc.4 . 2 (𝜑𝜏)
5 syl23anc.5 . . 3 (𝜑𝜂)
6 syl33anc.6 . . 3 (𝜑𝜁)
75, 6jca 511 . 2 (𝜑 → (𝜂𝜁))
8 syl312anc.7 . 2 (((𝜓𝜒𝜃) ∧ 𝜏 ∧ (𝜂𝜁)) → 𝜎)
91, 2, 3, 4, 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 207  df-an 396  df-3an 1088
This theorem is referenced by:  pythagtriplem19  16867  cdleme27cl  40349  cdlemefs27cl  40396  cdleme32fvcl  40423  cdlemg16ALTN  40641  cdlemg27a  40675  cdlemg31c  40682  cdlemg39  40699  cdlemk11ta  40912  cdlemk19ylem  40913  cdlemk11tc  40928  cdlemk45  40930  dihmeetlem12N  41301  dihjatc  41400  flt4lem5c  42641  flt4lem5d  42642  flt4lem5e  42643
  Copyright terms: Public domain W3C validator