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

Theorem syl311anc 1381
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 1125 . 2 (𝜑 → (𝜓𝜒𝜃))
5 syl3Xanc.4 . 2 (𝜑𝜏)
6 syl23anc.5 . 2 (𝜑𝜂)
7 syl311anc.6 . 2 (((𝜓𝜒𝜃) ∧ 𝜏𝜂) → 𝜁)
84, 5, 6, 7syl3anc 1368 1 (𝜑𝜁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1084
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 210  df-an 400  df-3an 1086
This theorem is referenced by:  syl312anc  1388  syl321anc  1389  syl313anc  1391  syl331anc  1392  pythagtrip  16169  nmolb2d  23331  nmoleub  23344  clwwisshclwwslem  27806  numclwwlk1lem2foa  28146  fprlem1  33198  cvlcvr1  36584  4atlem12b  36856  dalawlem10  37125  dalawlem13  37128  dalawlem15  37130  osumcllem11N  37211  lhp2atne  37279  lhp2at0ne  37281  cdlemd  37452  ltrneq3  37453  cdleme7d  37491  cdlemeg49le  37756  cdleme  37805  cdlemg1a  37815  ltrniotavalbN  37829  cdlemg44  37978  cdlemk19  38114  cdlemk27-3  38152  cdlemk33N  38154  cdlemk34  38155  cdlemk49  38196  cdlemk53a  38200  cdlemk19u  38215  cdlemk56w  38218  dia2dimlem4  38312  dih1dimatlem0  38573  itsclc0yqe  45106  itsclinecirc0  45118  itsclinecirc0b  45119  inlinecirc02plem  45131
  Copyright terms: Public domain W3C validator