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

Theorem syl113anc 1335
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 1240 . 2 (𝜑 → (𝜃𝜏𝜂))
7 syl113anc.6 . 2 ((𝜓𝜒 ∧ (𝜃𝜏𝜂)) → 𝜁)
81, 2, 6, 7syl3anc 1323 1 (𝜑𝜁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1036
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 386  df-3an 1038
This theorem is referenced by:  syl123anc  1340  syl213anc  1342  pythagtriplem18  15480  initoeu2  16606  psgnunilem1  17853  mulmarep1gsum1  20319  mulmarep1gsum2  20320  smadiadetlem4  20415  cramerimplem2  20430  cramerlem2  20434  cramer  20437  cnhaus  21098  dishaus  21126  ordthauslem  21127  pthaus  21381  txhaus  21390  xkohaus  21396  regr1lem  21482  methaus  22265  metnrmlem3  22604  f1otrge  25686  axpaschlem  25754  wwlksnwwlksnon  26713  n4cyclfrgr  27053  br8d  29306  lt2addrd  29399  xlt2addrd  29408  br8  31407  br4  31409  nosires  31630  btwnxfr  31858  lineext  31878  brsegle  31910  brsegle2  31911  lfl0  33871  lfladd  33872  lflsub  33873  lflmul  33874  lflnegcl  33881  lflvscl  33883  lkrlss  33901  3dimlem3  34266  3dimlem4  34269  3dim3  34274  2llnm3N  34374  2lplnja  34424  4atex  34881  4atex3  34886  trlval4  34994  cdleme7c  35051  cdleme7d  35052  cdleme7ga  35054  cdleme21h  35141  cdleme21i  35142  cdleme21j  35143  cdleme21  35144  cdleme32d  35251  cdleme32f  35253  cdleme35h2  35264  cdleme38m  35270  cdleme40m  35274  cdlemg8  35438  cdlemg11a  35444  cdlemg10a  35447  cdlemg12b  35451  cdlemg12d  35453  cdlemg12f  35455  cdlemg12g  35456  cdlemg15a  35462  cdlemg16  35464  cdlemg16z  35466  cdlemg18a  35485  cdlemg24  35495  cdlemg29  35512  cdlemg33b  35514  cdlemg38  35522  cdlemg39  35523  cdlemg40  35524  cdlemg44b  35539  cdlemj2  35629  cdlemk7  35655  cdlemk12  35657  cdlemk12u  35679  cdlemk32  35704  cdlemk25-3  35711  cdlemk34  35717  cdlemkid3N  35740  cdlemkid4  35741  cdlemk11t  35753  cdlemk53  35764  cdlemk55b  35767  cdleml3N  35785  hdmapln1  36717
  Copyright terms: Public domain W3C validator