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

Theorem syl311anc 1332
 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 1235 . 2 (𝜑 → (𝜓𝜒𝜃))
5 syl22anc.4 . 2 (𝜑𝜏)
6 syl23anc.5 . 2 (𝜑𝜂)
7 syl311anc.6 . 2 (((𝜓𝜒𝜃) ∧ 𝜏𝜂) → 𝜁)
84, 5, 6, 7syl3anc 1318 1 (𝜑𝜁)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ w3a 1031 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 196  df-an 385  df-3an 1033 This theorem is referenced by:  syl312anc  1339  syl321anc  1340  syl313anc  1342  syl331anc  1343  pythagtrip  15377  nmolb2d  22332  nmoleub  22345  clwwisshclwwlem  26334  cvlcvr1  33644  4atlem12b  33915  dalawlem10  34184  dalawlem13  34187  dalawlem15  34189  osumcllem11N  34270  lhp2atne  34338  lhp2at0ne  34340  cdlemd  34512  ltrneq3  34513  cdleme7d  34551  cdlemeg49le  34817  cdleme  34866  cdlemg1a  34876  ltrniotavalbN  34890  cdlemg44  35039  cdlemk19  35175  cdlemk27-3  35213  cdlemk33N  35215  cdlemk34  35216  cdlemk49  35257  cdlemk53a  35261  cdlemk19u  35276  cdlemk56w  35279  dia2dimlem4  35374  dih1dimatlem0  35635  clwwisshclwwslem  41234
 Copyright terms: Public domain W3C validator