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

Theorem syl312anc 1392
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 513 . 2 (𝜑 → (𝜂𝜁))
8 syl312anc.7 . 2 (((𝜓𝜒𝜃) ∧ 𝜏 ∧ (𝜂𝜁)) → 𝜎)
91, 2, 3, 4, 7, 8syl311anc 1385 1 (𝜑𝜎)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088
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 398  df-3an 1090
This theorem is referenced by:  pythagtriplem19  16766  cdleme27cl  39237  cdlemefs27cl  39284  cdleme32fvcl  39311  cdlemg16ALTN  39529  cdlemg27a  39563  cdlemg31c  39570  cdlemg39  39587  cdlemk11ta  39800  cdlemk19ylem  39801  cdlemk11tc  39816  cdlemk45  39818  dihmeetlem12N  40189  dihjatc  40288  flt4lem5c  41396  flt4lem5d  41397  flt4lem5e  41398
  Copyright terms: Public domain W3C validator