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

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

Proof of Theorem syl311anc
StepHypRef Expression
1 syl3anc.1 . . 3 (𝜑𝜓)
2 syl3anc.2 . . 3 (𝜑𝜒)
3 syl3anc.3 . . 3 (𝜑𝜃)
41, 2, 33jca 1119 . 2 (𝜑 → (𝜓𝜒𝜃))
5 syl3Xanc.4 . 2 (𝜑𝜏)
6 syl23anc.5 . 2 (𝜑𝜂)
7 syl311anc.6 . 2 (((𝜓𝜒𝜃) ∧ 𝜏𝜂) → 𝜁)
84, 5, 6, 7syl3anc 1439 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 199  df-an 387  df-3an 1073
This theorem is referenced by:  syl312anc  1459  syl321anc  1460  syl313anc  1462  syl331anc  1463  pythagtrip  15943  nmolb2d  22930  nmoleub  22943  clwwisshclwwslem  27403  numclwwlk1lem2foa  27783  numclwwlk1lem2foaOLD  27784  cvlcvr1  35487  4atlem12b  35759  dalawlem10  36028  dalawlem13  36031  dalawlem15  36033  osumcllem11N  36114  lhp2atne  36182  lhp2at0ne  36184  cdlemd  36355  ltrneq3  36356  cdleme7d  36394  cdlemeg49le  36659  cdleme  36708  cdlemg1a  36718  ltrniotavalbN  36732  cdlemg44  36881  cdlemk19  37017  cdlemk27-3  37055  cdlemk33N  37057  cdlemk34  37058  cdlemk49  37099  cdlemk53a  37103  cdlemk19u  37118  cdlemk56w  37121  dia2dimlem4  37215  dih1dimatlem0  37476  itsclc0yqe  43489  itsclinecirc0  43501  itsclinecirc0b  43502  inlinecirc02plem  43514
  Copyright terms: Public domain W3C validator