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

Theorem syl132anc 1200
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 518 . 2  |-  ( ph  ->  ( et  /\  ze ) )
8 syl132anc.7 . 2  |-  ( ( ps  /\  ( ch 
/\  th  /\  ta )  /\  ( et  /\  ze ) )  ->  si )
91, 2, 3, 4, 7, 8syl131anc 1195 1  |-  ( ph  ->  si )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  drsdirfi  14088  btwncomim  24708  btwnswapid  24712  btwnintr  24714  btwnexch3  24715  btwnxfr  24751  linecgrand  24777  btwnconn1lem13  24794  seglecgr12im  24805  segletr  24809  linethru  24848  lshpkrlem5  29926  omlmod1i2N  30072  omlspjN  30073  atcmp  30123  atexchcvrN  30251  atbtwn  30257  1cvratlt  30285  2atjlej  30290  hlatexch3N  30291  hlatexch4  30292  atcvrlln2  30330  atcvrlln  30331  llncmp  30333  llncvrlpln  30369  lplncmp  30373  lplnexllnN  30375  2llnjaN  30377  4atlem11  30420  lplncvrlvol  30427  lvolcmp  30428  dalem1  30470  dalem2  30472  dalem24  30508  dalem25  30509  dalem42  30525  lncvrat  30593  2llnma3r  30599  lhp2lt  30812  4atexlemswapqr  30874  4atexlemtlw  30878  4atexlemntlpq  30879  4atexlemc  30880  4atexlemnclw  30881  4atexlemcnd  30883  4atex2  30888  cdlemd1  31009  cdlemd7  31015  cdleme0e  31028  cdleme7c  31056  cdleme7d  31057  cdleme7e  31058  cdleme7ga  31059  cdleme7  31060  cdleme16aN  31070  cdleme11c  31072  cdleme11e  31074  cdleme11l  31080  cdleme11  31081  cdleme14  31084  cdleme15a  31085  cdleme16b  31090  cdleme16c  31091  cdleme16d  31092  cdleme16e  31093  cdleme16f  31094  cdleme18b  31103  cdleme19d  31117  cdleme20d  31123  cdleme20f  31125  cdleme20h  31127  cdleme20l1  31131  cdleme20l2  31132  cdleme20l  31133  cdleme21a  31136  cdleme21b  31137  cdleme21c  31138  cdleme21ct  31140  cdleme22f2  31158  cdleme22g  31159  cdlemefr32sn2aw  31215  cdleme43fsv1snlem  31231  cdleme32b  31253  cdleme35a  31259  cdleme35f  31265  cdleme36m  31272  cdleme37m  31273  cdleme42k  31295  cdleme43bN  31301  cdleme17d2  31306  cdlemeg46req  31340  cdlemeg46gfv  31341  cdlemeg46gfre  31343  cdleme50trn2a  31361  cdleme50trn2  31362  cdlemg8b  31439  cdlemg10a  31451  cdlemg12d  31457  cdlemg13a  31462  cdlemg15  31467  cdlemg16z  31470  cdlemg18b  31490  cdlemg18c  31491  cdlemg18  31493  cdlemg27b  31507  cdlemg33  31522  cdlemg42  31540  trljco  31551  cdlemj3  31634  tendoid0  31636  cdlemk3  31644  cdlemk22  31704  cdlemk36  31724  cdlemkfid3N  31736  cdlemk47  31760  cdlemk48  31761  cdlemk49  31762  cdlemk50  31763  cdlemk51  31764  cdlemk52  31765  cdlemk53a  31766  cdlemk53b  31767  cdlemk53  31768  cdlemk54  31769  cdlemk55  31772  cdlemk35u  31775  cdlemk39u1  31778  cdleml3N  31789
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