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

Theorem syl113anc 1329
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
syl12anc.1 (𝜑𝜓)
syl12anc.2 (𝜑𝜒)
syl12anc.3 (𝜑𝜃)
syl22anc.4 (𝜑𝜏)
syl23anc.5 (𝜑𝜂)
syl113anc.6 ((𝜓𝜒 ∧ (𝜃𝜏𝜂)) → 𝜁)
Assertion
Ref Expression
syl113anc (𝜑𝜁)

Proof of Theorem syl113anc
StepHypRef Expression
1 syl12anc.1 . 2 (𝜑𝜓)
2 syl12anc.2 . 2 (𝜑𝜒)
3 syl12anc.3 . . 3 (𝜑𝜃)
4 syl22anc.4 . . 3 (𝜑𝜏)
5 syl23anc.5 . . 3 (𝜑𝜂)
63, 4, 53jca 1234 . 2 (𝜑 → (𝜃𝜏𝜂))
7 syl113anc.6 . 2 ((𝜓𝜒 ∧ (𝜃𝜏𝜂)) → 𝜁)
81, 2, 6, 7syl3anc 1317 1 (𝜑𝜁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1030
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 195  df-an 384  df-3an 1032
This theorem is referenced by:  syl123anc  1334  syl213anc  1336  pythagtriplem18  15317  initoeu2  16431  psgnunilem1  17678  mulmarep1gsum1  20136  mulmarep1gsum2  20137  smadiadetlem4  20232  cramerimplem2  20247  cramerlem2  20251  cramer  20254  cnhaus  20906  dishaus  20934  ordthauslem  20935  pthaus  21189  txhaus  21198  xkohaus  21204  regr1lem  21290  methaus  22072  metnrmlem3  22399  f1otrge  25466  axpaschlem  25534  n4cyclfrgra  26307  br8d  28604  lt2addrd  28705  xlt2addrd  28715  br8  30701  br4  30703  btwnxfr  31135  lineext  31155  brsegle  31187  brsegle2  31188  lfl0  33169  lfladd  33170  lflsub  33171  lflmul  33172  lflnegcl  33179  lflvscl  33181  lkrlss  33199  3dimlem3  33564  3dimlem4  33567  3dim3  33572  2llnm3N  33672  2lplnja  33722  4atex  34179  4atex3  34184  trlval4  34292  cdleme7c  34349  cdleme7d  34350  cdleme7ga  34352  cdleme21h  34439  cdleme21i  34440  cdleme21j  34441  cdleme21  34442  cdleme32d  34549  cdleme32f  34551  cdleme35h2  34562  cdleme38m  34568  cdleme40m  34572  cdlemg8  34736  cdlemg11a  34742  cdlemg10a  34745  cdlemg12b  34749  cdlemg12d  34751  cdlemg12f  34753  cdlemg12g  34754  cdlemg15a  34760  cdlemg16  34762  cdlemg16z  34764  cdlemg18a  34783  cdlemg24  34793  cdlemg29  34810  cdlemg33b  34812  cdlemg38  34820  cdlemg39  34821  cdlemg40  34822  cdlemg44b  34837  cdlemj2  34927  cdlemk7  34953  cdlemk12  34955  cdlemk12u  34977  cdlemk32  35002  cdlemk25-3  35009  cdlemk34  35015  cdlemkid3N  35038  cdlemkid4  35039  cdlemk11t  35051  cdlemk53  35062  cdlemk55b  35065  cdleml3N  35083  hdmapln1  36015  wwlksnwwlksnon  41119  n4cyclfrgr  41459
  Copyright terms: Public domain W3C validator