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

Theorem syl311anc 1337
 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 1240 . 2 (𝜑 → (𝜓𝜒𝜃))
5 syl22anc.4 . 2 (𝜑𝜏)
6 syl23anc.5 . 2 (𝜑𝜂)
7 syl311anc.6 . 2 (((𝜓𝜒𝜃) ∧ 𝜏𝜂) → 𝜁)
84, 5, 6, 7syl3anc 1323 1 (𝜑𝜁)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ w3a 1036 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 386  df-3an 1038 This theorem is referenced by:  syl312anc  1344  syl321anc  1345  syl313anc  1347  syl331anc  1348  pythagtrip  15466  nmolb2d  22435  nmoleub  22448  clwwisshclwwslem  26800  cvlcvr1  34127  4atlem12b  34398  dalawlem10  34667  dalawlem13  34670  dalawlem15  34672  osumcllem11N  34753  lhp2atne  34821  lhp2at0ne  34823  cdlemd  34995  ltrneq3  34996  cdleme7d  35034  cdlemeg49le  35300  cdleme  35349  cdlemg1a  35359  ltrniotavalbN  35373  cdlemg44  35522  cdlemk19  35658  cdlemk27-3  35696  cdlemk33N  35698  cdlemk34  35699  cdlemk49  35740  cdlemk53a  35744  cdlemk19u  35759  cdlemk56w  35762  dia2dimlem4  35857  dih1dimatlem0  36118
 Copyright terms: Public domain W3C validator