MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl132anc 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  14350  qqhval2lem  24318  qqhghm  24325  qqhrhm  24326  btwncomim  25851  btwnswapid  25855  btwnintr  25857  btwnexch3  25858  btwnxfr  25894  linecgrand  25920  btwnconn1lem13  25937  seglecgr12im  25948  segletr  25952  linethru  25991  lshpkrlem5  29597  omlmod1i2N  29743  omlspjN  29744  atcmp  29794  atexchcvrN  29922  atbtwn  29928  1cvratlt  29956  2atjlej  29961  hlatexch3N  29962  hlatexch4  29963  atcvrlln2  30001  atcvrlln  30002  llncmp  30004  llncvrlpln  30040  lplncmp  30044  lplnexllnN  30046  2llnjaN  30048  4atlem11  30091  lplncvrlvol  30098  lvolcmp  30099  dalem1  30141  dalem2  30143  dalem24  30179  dalem25  30180  dalem42  30196  lncvrat  30264  2llnma3r  30270  lhp2lt  30483  4atexlemswapqr  30545  4atexlemtlw  30549  4atexlemntlpq  30550  4atexlemc  30551  4atexlemnclw  30552  4atexlemcnd  30554  4atex2  30559  cdlemd1  30680  cdlemd7  30686  cdleme0e  30699  cdleme7c  30727  cdleme7d  30728  cdleme7e  30729  cdleme7ga  30730  cdleme7  30731  cdleme16aN  30741  cdleme11c  30743  cdleme11e  30745  cdleme11l  30751  cdleme11  30752  cdleme14  30755  cdleme15a  30756  cdleme16b  30761  cdleme16c  30762  cdleme16d  30763  cdleme16e  30764  cdleme16f  30765  cdleme18b  30774  cdleme19d  30788  cdleme20d  30794  cdleme20f  30796  cdleme20h  30798  cdleme20l1  30802  cdleme20l2  30803  cdleme20l  30804  cdleme21a  30807  cdleme21b  30808  cdleme21c  30809  cdleme21ct  30811  cdleme22f2  30829  cdleme22g  30830  cdlemefr32sn2aw  30886  cdleme43fsv1snlem  30902  cdleme32b  30924  cdleme35a  30930  cdleme35f  30936  cdleme36m  30943  cdleme37m  30944  cdleme42k  30966  cdleme43bN  30972  cdleme17d2  30977  cdlemeg46req  31011  cdlemeg46gfv  31012  cdlemeg46gfre  31014  cdleme50trn2a  31032  cdleme50trn2  31033  cdlemg8b  31110  cdlemg10a  31122  cdlemg12d  31128  cdlemg13a  31133  cdlemg15  31138  cdlemg16z  31141  cdlemg18b  31161  cdlemg18c  31162  cdlemg18  31164  cdlemg27b  31178  cdlemg33  31193  cdlemg42  31211  trljco  31222  cdlemj3  31305  tendoid0  31307  cdlemk3  31315  cdlemk22  31375  cdlemk36  31395  cdlemkfid3N  31407  cdlemk47  31431  cdlemk48  31432  cdlemk49  31433  cdlemk50  31434  cdlemk51  31435  cdlemk52  31436  cdlemk53a  31437  cdlemk53b  31438  cdlemk53  31439  cdlemk54  31440  cdlemk55  31443  cdlemk35u  31446  cdlemk39u1  31449  cdleml3N  31460
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