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

Theorem syl311anc 1489
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 1121 . 2 (𝜑 → (𝜓𝜒𝜃))
5 syl22anc.4 . 2 (𝜑𝜏)
6 syl23anc.5 . 2 (𝜑𝜂)
7 syl311anc.6 . 2 (((𝜓𝜒𝜃) ∧ 𝜏𝜂) → 𝜁)
84, 5, 6, 7syl3anc 1475 1 (𝜑𝜁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1070
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 1072
This theorem is referenced by:  syl312anc  1496  syl321anc  1497  syl313anc  1499  syl331anc  1500  pythagtrip  15745  nmolb2d  22741  nmoleub  22754  clwwisshclwwslem  27161  numclwlk1lem2foa  27538  cvlcvr1  35141  4atlem12b  35412  dalawlem10  35681  dalawlem13  35684  dalawlem15  35686  osumcllem11N  35767  lhp2atne  35835  lhp2at0ne  35837  cdlemd  36009  ltrneq3  36010  cdleme7d  36048  cdlemeg49le  36313  cdleme  36362  cdlemg1a  36372  ltrniotavalbN  36386  cdlemg44  36535  cdlemk19  36671  cdlemk27-3  36709  cdlemk33N  36711  cdlemk34  36712  cdlemk49  36753  cdlemk53a  36757  cdlemk19u  36772  cdlemk56w  36775  dia2dimlem4  36870  dih1dimatlem0  37131
  Copyright terms: Public domain W3C validator