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

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

Proof of Theorem syl311anc
StepHypRef Expression
1 syl12anc.1 . . 3 (𝜑𝜓)
2 syl12anc.2 . . 3 (𝜑𝜒)
3 syl12anc.3 . . 3 (𝜑𝜃)
41, 2, 33jca 1122 . 2 (𝜑 → (𝜓𝜒𝜃))
5 syl22anc.4 . 2 (𝜑𝜏)
6 syl23anc.5 . 2 (𝜑𝜂)
7 syl311anc.6 . 2 (((𝜓𝜒𝜃) ∧ 𝜏𝜂) → 𝜁)
84, 5, 6, 7syl3anc 1476 1 (𝜑𝜁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1071
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 197  df-an 383  df-3an 1073
This theorem is referenced by:  syl312anc  1497  syl321anc  1498  syl313anc  1500  syl331anc  1501  pythagtrip  15746  nmolb2d  22742  nmoleub  22755  clwwisshclwwslem  27164  numclwwlk1lem2foa  27540  cvlcvr1  35148  4atlem12b  35419  dalawlem10  35688  dalawlem13  35691  dalawlem15  35693  osumcllem11N  35774  lhp2atne  35842  lhp2at0ne  35844  cdlemd  36016  ltrneq3  36017  cdleme7d  36055  cdlemeg49le  36320  cdleme  36369  cdlemg1a  36379  ltrniotavalbN  36393  cdlemg44  36542  cdlemk19  36678  cdlemk27-3  36716  cdlemk33N  36718  cdlemk34  36719  cdlemk49  36760  cdlemk53a  36764  cdlemk19u  36779  cdlemk56w  36782  dia2dimlem4  36877  dih1dimatlem0  37138
  Copyright terms: Public domain W3C validator