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

Theorem syl113anc 1231
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 1168 . 2  |-  ( ph  ->  ( th  /\  ta  /\  et ) )
7 syl113anc.6 . 2  |-  ( ( ps  /\  ch  /\  ( th  /\  ta  /\  et ) )  ->  ze )
81, 2, 6, 7syl3anc 1219 1  |-  ( ph  ->  ze )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 965
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 185  df-an 371  df-3an 967
This theorem is referenced by:  syl123anc  1236  syl213anc  1238  pythagtriplem18  14010  psgnunilem1  16110  mulmarep1gsum1  18504  mulmarep1gsum2  18505  smadiadetlem4  18600  cramerimplem2  18615  cramerlem2  18619  cramer  18622  cnhaus  19083  dishaus  19111  ordthauslem  19112  pthaus  19336  txhaus  19345  xkohaus  19351  regr1lem  19437  methaus  20220  metnrmlem3  20562  axpaschlem  23331  br8d  26086  lt2addrd  26180  xlt2addrd  26195  br8  27703  br4  27705  btwnxfr  28224  lineext  28244  brsegle  28276  brsegle2  28277  n4cyclfrgra  30751  lfl0  33019  lfladd  33020  lflsub  33021  lflmul  33022  lflnegcl  33029  lflvscl  33031  lkrlss  33049  3dimlem3  33414  3dimlem4  33417  3dim3  33422  2llnm3N  33522  2lplnja  33572  4atex  34029  4atex3  34034  trlval4  34141  cdleme7c  34198  cdleme7d  34199  cdleme7ga  34201  cdleme21h  34287  cdleme21i  34288  cdleme21j  34289  cdleme21  34290  cdleme32d  34397  cdleme32f  34399  cdleme35h2  34410  cdleme38m  34416  cdleme40m  34420  cdlemg8  34584  cdlemg11a  34590  cdlemg10a  34593  cdlemg12b  34597  cdlemg12d  34599  cdlemg12f  34601  cdlemg12g  34602  cdlemg15a  34608  cdlemg16  34610  cdlemg16z  34612  cdlemg18a  34631  cdlemg24  34641  cdlemg29  34658  cdlemg33b  34660  cdlemg38  34668  cdlemg39  34669  cdlemg40  34670  cdlemg44b  34685  cdlemj2  34775  cdlemk7  34801  cdlemk12  34803  cdlemk12u  34825  cdlemk32  34850  cdlemk25-3  34857  cdlemk34  34863  cdlemkid3N  34886  cdlemkid4  34887  cdlemk11t  34899  cdlemk53  34910  cdlemk55b  34913  cdleml3N  34931  hdmapln1  35863
  Copyright terms: Public domain W3C validator