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

Theorem syl113anc 1194
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
sylXanc.1  |-  ( ph  ->  ps )
sylXanc.2  |-  ( ph  ->  ch )
sylXanc.3  |-  ( ph  ->  th )
sylXanc.4  |-  ( ph  ->  ta )
sylXanc.5  |-  ( ph  ->  et )
syl113anc.6  |-  ( ( ps  /\  ch  /\  ( th  /\  ta  /\  et ) )  ->  ze )
Assertion
Ref Expression
syl113anc  |-  ( ph  ->  ze )

Proof of Theorem syl113anc
StepHypRef Expression
1 sylXanc.1 . 2  |-  ( ph  ->  ps )
2 sylXanc.2 . 2  |-  ( ph  ->  ch )
3 sylXanc.3 . . 3  |-  ( ph  ->  th )
4 sylXanc.4 . . 3  |-  ( ph  ->  ta )
5 sylXanc.5 . . 3  |-  ( ph  ->  et )
63, 4, 53jca 1132 . 2  |-  ( ph  ->  ( th  /\  ta  /\  et ) )
7 syl113anc.6 . 2  |-  ( ( ps  /\  ch  /\  ( th  /\  ta  /\  et ) )  ->  ze )
81, 2, 6, 7syl3anc 1182 1  |-  ( ph  ->  ze )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  syl123anc  1199  syl213anc  1201  pythagtriplem18  12885  cnhaus  17082  dishaus  17110  ordthauslem  17111  pthaus  17332  txhaus  17341  xkohaus  17347  regr1lem  17430  methaus  18066  metnrmlem3  18365  br8  24113  br4  24115  axpaschlem  24568  btwnxfr  24679  lineext  24699  brsegle  24731  brsegle2  24732  psgnunilem1  27416  lfl0  29255  lfladd  29256  lflsub  29257  lflmul  29258  lflnegcl  29265  lflvscl  29267  lkrlss  29285  3dimlem3  29650  3dimlem4  29653  3dim3  29658  2llnm3N  29758  2lplnja  29808  4atex  30265  4atex3  30270  trlval4  30377  cdleme7c  30434  cdleme7d  30435  cdleme7ga  30437  cdleme21h  30523  cdleme21i  30524  cdleme21j  30525  cdleme21  30526  cdleme32d  30633  cdleme32f  30635  cdleme35h2  30646  cdleme38m  30652  cdleme40m  30656  cdlemg8  30820  cdlemg11a  30826  cdlemg10a  30829  cdlemg12b  30833  cdlemg12d  30835  cdlemg12f  30837  cdlemg12g  30838  cdlemg15a  30844  cdlemg16  30846  cdlemg16z  30848  cdlemg18a  30867  cdlemg24  30877  cdlemg29  30894  cdlemg33b  30896  cdlemg38  30904  cdlemg39  30905  cdlemg40  30906  cdlemg44b  30921  cdlemj2  31011  cdlemk7  31037  cdlemk12  31039  cdlemk12u  31061  cdlemk32  31086  cdlemk25-3  31093  cdlemk34  31099  cdlemkid3N  31122  cdlemkid4  31123  cdlemk11t  31135  cdlemk53  31146  cdlemk55b  31149  cdleml3N  31167  hdmapln1  32099
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator