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 206  df-an 395  df-3an 1086
This theorem is referenced by:  syl312anc  1388  syl321anc  1389  syl313anc  1391  syl331anc  1392  fprlem1  8306  pythagtrip  16806  nmolb2d  24679  nmoleub  24692  clwwisshclwwslem  29896  numclwwlk1lem2foa  30236  cvlcvr1  38941  4atlem12b  39214  dalawlem10  39483  dalawlem13  39486  dalawlem15  39488  osumcllem11N  39569  lhp2atne  39637  lhp2at0ne  39639  cdlemd  39810  ltrneq3  39811  cdleme7d  39849  cdlemeg49le  40114  cdleme  40163  cdlemg1a  40173  ltrniotavalbN  40187  cdlemg44  40336  cdlemk19  40472  cdlemk27-3  40510  cdlemk33N  40512  cdlemk34  40513  cdlemk49  40554  cdlemk53a  40558  cdlemk19u  40573  cdlemk56w  40576  dia2dimlem4  40670  dih1dimatlem0  40931  itsclc0yqe  48020  itsclinecirc0  48032  itsclinecirc0b  48033  inlinecirc02plem  48045
  Copyright terms: Public domain W3C validator