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  14072  btwncomim  24636  btwnswapid  24640  btwnintr  24642  btwnexch3  24643  btwnxfr  24679  linecgrand  24705  btwnconn1lem13  24722  seglecgr12im  24733  segletr  24737  linethru  24776  lshpkrlem5  29304  omlmod1i2N  29450  omlspjN  29451  atcmp  29501  atexchcvrN  29629  atbtwn  29635  1cvratlt  29663  2atjlej  29668  hlatexch3N  29669  hlatexch4  29670  atcvrlln2  29708  atcvrlln  29709  llncmp  29711  llncvrlpln  29747  lplncmp  29751  lplnexllnN  29753  2llnjaN  29755  4atlem11  29798  lplncvrlvol  29805  lvolcmp  29806  dalem1  29848  dalem2  29850  dalem24  29886  dalem25  29887  dalem42  29903  lncvrat  29971  2llnma3r  29977  lhp2lt  30190  4atexlemswapqr  30252  4atexlemtlw  30256  4atexlemntlpq  30257  4atexlemc  30258  4atexlemnclw  30259  4atexlemcnd  30261  4atex2  30266  cdlemd1  30387  cdlemd7  30393  cdleme0e  30406  cdleme7c  30434  cdleme7d  30435  cdleme7e  30436  cdleme7ga  30437  cdleme7  30438  cdleme16aN  30448  cdleme11c  30450  cdleme11e  30452  cdleme11l  30458  cdleme11  30459  cdleme14  30462  cdleme15a  30463  cdleme16b  30468  cdleme16c  30469  cdleme16d  30470  cdleme16e  30471  cdleme16f  30472  cdleme18b  30481  cdleme19d  30495  cdleme20d  30501  cdleme20f  30503  cdleme20h  30505  cdleme20l1  30509  cdleme20l2  30510  cdleme20l  30511  cdleme21a  30514  cdleme21b  30515  cdleme21c  30516  cdleme21ct  30518  cdleme22f2  30536  cdleme22g  30537  cdlemefr32sn2aw  30593  cdleme43fsv1snlem  30609  cdleme32b  30631  cdleme35a  30637  cdleme35f  30643  cdleme36m  30650  cdleme37m  30651  cdleme42k  30673  cdleme43bN  30679  cdleme17d2  30684  cdlemeg46req  30718  cdlemeg46gfv  30719  cdlemeg46gfre  30721  cdleme50trn2a  30739  cdleme50trn2  30740  cdlemg8b  30817  cdlemg10a  30829  cdlemg12d  30835  cdlemg13a  30840  cdlemg15  30845  cdlemg16z  30848  cdlemg18b  30868  cdlemg18c  30869  cdlemg18  30871  cdlemg27b  30885  cdlemg33  30900  cdlemg42  30918  trljco  30929  cdlemj3  31012  tendoid0  31014  cdlemk3  31022  cdlemk22  31082  cdlemk36  31102  cdlemkfid3N  31114  cdlemk47  31138  cdlemk48  31139  cdlemk49  31140  cdlemk50  31141  cdlemk51  31142  cdlemk52  31143  cdlemk53a  31144  cdlemk53b  31145  cdlemk53  31146  cdlemk54  31147  cdlemk55  31150  cdlemk35u  31153  cdlemk39u1  31156  cdleml3N  31167
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