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

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

Proof of Theorem syl132anc
StepHypRef Expression
1 sylXanc.1 . 2  |-  ( ph  ->  ps )
2 sylXanc.2 . 2  |-  ( ph  ->  ch )
3 sylXanc.3 . 2  |-  ( ph  ->  th )
4 sylXanc.4 . 2  |-  ( ph  ->  ta )
5 sylXanc.5 . . 3  |-  ( ph  ->  et )
6 sylXanc.6 . . 3  |-  ( ph  ->  ze )
75, 6jca 519 . 2  |-  ( ph  ->  ( et  /\  ze ) )
8 syl132anc.7 . 2  |-  ( ( ps  /\  ( ch 
/\  th  /\  ta )  /\  ( et  /\  ze ) )  ->  si )
91, 2, 3, 4, 7, 8syl131anc 1197 1  |-  ( ph  ->  si )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  drsdirfi  14387  qqhval2lem  24357  qqhghm  24364  qqhrhm  24365  btwncomim  25939  btwnswapid  25943  btwnintr  25945  btwnexch3  25946  btwnxfr  25982  linecgrand  26008  btwnconn1lem13  26025  seglecgr12im  26036  segletr  26040  linethru  26079  lshpkrlem5  29849  omlmod1i2N  29995  omlspjN  29996  atcmp  30046  atexchcvrN  30174  atbtwn  30180  1cvratlt  30208  2atjlej  30213  hlatexch3N  30214  hlatexch4  30215  atcvrlln2  30253  atcvrlln  30254  llncmp  30256  llncvrlpln  30292  lplncmp  30296  lplnexllnN  30298  2llnjaN  30300  4atlem11  30343  lplncvrlvol  30350  lvolcmp  30351  dalem1  30393  dalem2  30395  dalem24  30431  dalem25  30432  dalem42  30448  lncvrat  30516  2llnma3r  30522  lhp2lt  30735  4atexlemswapqr  30797  4atexlemtlw  30801  4atexlemntlpq  30802  4atexlemc  30803  4atexlemnclw  30804  4atexlemcnd  30806  4atex2  30811  cdlemd1  30932  cdlemd7  30938  cdleme0e  30951  cdleme7c  30979  cdleme7d  30980  cdleme7e  30981  cdleme7ga  30982  cdleme7  30983  cdleme16aN  30993  cdleme11c  30995  cdleme11e  30997  cdleme11l  31003  cdleme11  31004  cdleme14  31007  cdleme15a  31008  cdleme16b  31013  cdleme16c  31014  cdleme16d  31015  cdleme16e  31016  cdleme16f  31017  cdleme18b  31026  cdleme19d  31040  cdleme20d  31046  cdleme20f  31048  cdleme20h  31050  cdleme20l1  31054  cdleme20l2  31055  cdleme20l  31056  cdleme21a  31059  cdleme21b  31060  cdleme21c  31061  cdleme21ct  31063  cdleme22f2  31081  cdleme22g  31082  cdlemefr32sn2aw  31138  cdleme43fsv1snlem  31154  cdleme32b  31176  cdleme35a  31182  cdleme35f  31188  cdleme36m  31195  cdleme37m  31196  cdleme42k  31218  cdleme43bN  31224  cdleme17d2  31229  cdlemeg46req  31263  cdlemeg46gfv  31264  cdlemeg46gfre  31266  cdleme50trn2a  31284  cdleme50trn2  31285  cdlemg8b  31362  cdlemg10a  31374  cdlemg12d  31380  cdlemg13a  31385  cdlemg15  31390  cdlemg16z  31393  cdlemg18b  31413  cdlemg18c  31414  cdlemg18  31416  cdlemg27b  31430  cdlemg33  31445  cdlemg42  31463  trljco  31474  cdlemj3  31557  tendoid0  31559  cdlemk3  31567  cdlemk22  31627  cdlemk36  31647  cdlemkfid3N  31659  cdlemk47  31683  cdlemk48  31684  cdlemk49  31685  cdlemk50  31686  cdlemk51  31687  cdlemk52  31688  cdlemk53a  31689  cdlemk53b  31690  cdlemk53  31691  cdlemk54  31692  cdlemk55  31695  cdlemk35u  31698  cdlemk39u1  31701  cdleml3N  31712
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator