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

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

Proof of Theorem syl113anc
StepHypRef Expression
1 syl3anc.1 . 2 (𝜑𝜓)
2 syl3anc.2 . 2 (𝜑𝜒)
3 syl3anc.3 . . 3 (𝜑𝜃)
4 syl3Xanc.4 . . 3 (𝜑𝜏)
5 syl23anc.5 . . 3 (𝜑𝜂)
63, 4, 53jca 1125 . 2 (𝜑 → (𝜃𝜏𝜂))
7 syl113anc.6 . 2 ((𝜓𝜒 ∧ (𝜃𝜏𝜂)) → 𝜁)
81, 2, 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:  syl123anc  1384  syl213anc  1386  pythagtriplem18  16146  initoeu2  17254  psgnunilem1  18599  mulmarep1gsum1  21157  mulmarep1gsum2  21158  smadiadetlem4  21253  cramerimplem2  21268  cramerlem2  21272  cramer  21275  cnhaus  21937  dishaus  21965  ordthauslem  21966  pthaus  22221  txhaus  22230  xkohaus  22236  regr1lem  22322  methaus  23105  metnrmlem3  23444  iscgrad  26583  f1otrge  26644  axpaschlem  26712  wwlksnwwlksnon  27679  n4cyclfrgr  28054  br8d  30347  lt2addrd  30461  xlt2addrd  30468  br8  32999  br4  33001  nosupres  33214  nosupbnd1lem1  33215  nosupbnd2  33223  btwnxfr  33524  lineext  33544  brsegle  33576  brsegle2  33577  lfl0  36241  lfladd  36242  lflsub  36243  lflmul  36244  lflnegcl  36251  lflvscl  36253  lkrlss  36271  3dimlem3  36637  3dimlem4  36640  3dim3  36645  2llnm3N  36745  2lplnja  36795  4atex  37252  4atex3  37257  trlval4  37364  cdleme7c  37421  cdleme7d  37422  cdleme7ga  37424  cdleme21h  37510  cdleme21i  37511  cdleme21j  37512  cdleme21  37513  cdleme32d  37620  cdleme32f  37622  cdleme35h2  37633  cdleme38m  37639  cdleme40m  37643  cdlemg8  37807  cdlemg11a  37813  cdlemg10a  37816  cdlemg12b  37820  cdlemg12d  37822  cdlemg12f  37824  cdlemg12g  37825  cdlemg15a  37831  cdlemg16  37833  cdlemg16z  37835  cdlemg18a  37854  cdlemg24  37864  cdlemg29  37881  cdlemg33b  37883  cdlemg38  37891  cdlemg39  37892  cdlemg40  37893  cdlemg44b  37908  cdlemj2  37998  cdlemk7  38024  cdlemk12  38026  cdlemk12u  38048  cdlemk32  38073  cdlemk25-3  38080  cdlemk34  38086  cdlemkid3N  38109  cdlemkid4  38110  cdlemk11t  38122  cdlemk53  38133  cdlemk55b  38136  cdleml3N  38154  hdmapln1  39082
  Copyright terms: Public domain W3C validator