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

Theorem syl113anc 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 (𝜑𝜂)
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 1123 . 2 (𝜑 → (𝜃𝜏𝜂))
7 syl113anc.6 . 2 ((𝜓𝜒 ∧ (𝜃𝜏𝜂)) → 𝜁)
81, 2, 6, 7syl3anc 1477 1 (𝜑𝜁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1072
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 385  df-3an 1074
This theorem is referenced by:  syl123anc  1494  syl213anc  1496  pythagtriplem18  15760  initoeu2  16888  psgnunilem1  18134  mulmarep1gsum1  20602  mulmarep1gsum2  20603  smadiadetlem4  20698  cramerimplem2  20713  cramerlem2  20717  cramer  20720  cnhaus  21381  dishaus  21409  ordthauslem  21410  pthaus  21664  txhaus  21673  xkohaus  21679  regr1lem  21765  methaus  22547  metnrmlem3  22886  f1otrge  25973  axpaschlem  26041  wwlksnwwlksnon  27055  wwlksnwwlksnonOLD  27057  n4cyclfrgr  27467  br8d  29751  lt2addrd  29847  xlt2addrd  29854  br8  31975  br4  31977  nosupres  32181  nosupbnd1lem1  32182  nosupbnd2  32190  btwnxfr  32491  lineext  32511  brsegle  32543  brsegle2  32544  lfl0  34874  lfladd  34875  lflsub  34876  lflmul  34877  lflnegcl  34884  lflvscl  34886  lkrlss  34904  3dimlem3  35269  3dimlem4  35272  3dim3  35277  2llnm3N  35377  2lplnja  35427  4atex  35884  4atex3  35889  trlval4  35997  cdleme7c  36054  cdleme7d  36055  cdleme7ga  36057  cdleme21h  36143  cdleme21i  36144  cdleme21j  36145  cdleme21  36146  cdleme32d  36253  cdleme32f  36255  cdleme35h2  36266  cdleme38m  36272  cdleme40m  36276  cdlemg8  36440  cdlemg11a  36446  cdlemg10a  36449  cdlemg12b  36453  cdlemg12d  36455  cdlemg12f  36457  cdlemg12g  36458  cdlemg15a  36464  cdlemg16  36466  cdlemg16z  36468  cdlemg18a  36487  cdlemg24  36497  cdlemg29  36514  cdlemg33b  36516  cdlemg38  36524  cdlemg39  36525  cdlemg40  36526  cdlemg44b  36541  cdlemj2  36631  cdlemk7  36657  cdlemk12  36659  cdlemk12u  36681  cdlemk32  36706  cdlemk25-3  36713  cdlemk34  36719  cdlemkid3N  36742  cdlemkid4  36743  cdlemk11t  36755  cdlemk53  36766  cdlemk55b  36769  cdleml3N  36787  hdmapln1  37719
  Copyright terms: Public domain W3C validator