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

Theorem syl121anc 1187
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 )
syl121anc.5  |-  ( ( ps  /\  ( ch 
/\  th )  /\  ta )  ->  et )
Assertion
Ref Expression
syl121anc  |-  ( ph  ->  et )

Proof of Theorem syl121anc
StepHypRef Expression
1 sylXanc.1 . 2  |-  ( ph  ->  ps )
2 sylXanc.2 . . 3  |-  ( ph  ->  ch )
3 sylXanc.3 . . 3  |-  ( ph  ->  th )
42, 3jca 518 . 2  |-  ( ph  ->  ( ch  /\  th ) )
5 sylXanc.4 . 2  |-  ( ph  ->  ta )
6 syl121anc.5 . 2  |-  ( ( ps  /\  ( ch 
/\  th )  /\  ta )  ->  et )
71, 4, 5, 6syl3anc 1182 1  |-  ( ph  ->  et )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  syl122anc  1191  disjxiun  4020  tfisi  4649  fsnunf2  5719  axdc4lem  8081  div32d  9559  div13d  9560  expdivd  11259  pcqmul  12906  pcid  12925  pcneg  12926  pc2dvds  12931  pcz  12933  pcaddlem  12936  pcadd  12937  pcmpt2  12941  pcbc  12948  qexpz  12949  expnprm  12950  spwpr4c  14341  sylow1lem1  14909  lmodvsnegOLD  15668  lspsneleq  15868  lspsneq  15875  lspfixed  15881  ssblex  17974  prdsxmslem2  18075  voliunlem1  18907  deg1mul3le  19502  deg1pw  19506  fta1blem  19554  bcmono  20516  dchrisum0flblem1  20657  dchrisum0flblem2  20658  pntibndlem1  20738  pntlemr  20751  nv1  21242  measxun  23539  btwnconn1lem14  24723  segcon2  24728  seglelin  24739  toplat  25290  islimrs4  25582  idmon  25817  cmp2morpcats  25961  cmpmorass  25966  cmpidmor2  25969  cmpidmor3  25970  neibastop3  26311  upixp  26403  fdc  26455  eldioph2b  26842  jm2.19lem4  27085  jm2.19  27086  jm2.26a  27093  jm2.26  27095  hbtlem2  27328  eqlkr3  29291  lkrshp  29295  lfl1dim  29311  lfl1dim2N  29312  eqlkr4  29355  2llnneN  29598  3dim2  29657  4atlem3  29785  4atlem11  29798  4atlem12  29801  pexmidlem4N  30162  lhp2at0nle  30224  lhple  30231  ltrnideq  30364  cdlemd9  30395  cdleme0ex2N  30413  cdleme0moN  30414  cdleme11a  30449  cdleme30a  30567  cdlemefs32sn1aw  30603  cdleme43fsv1snlem  30609  cdlemefs31fv1  30613  cdlemefs45eN  30620  cdleme41sn3a  30622  cdleme35h  30645  cdleme36a  30649  cdleme40m  30656  cdleme40n  30657  cdleme41sn3aw  30663  cdleme42h  30671  cdleme42k  30673  cdleme42mN  30676  cdleme43cN  30680  cdleme17d3  30685  cdleme48fvg  30689  cdlemeg47rv2  30699  cdlemeg46c  30702  cdlemeg46sfg  30709  cdlemeg46rjgN  30711  cdlemeg46rgv  30717  cdlemeg46req  30718  cdlemeg46gfv  30719  cdlemeg46gfre  30721  cdlemeg49lebilem  30728  cdleme50trn2  30740  cdlemg2kq  30791  cdlemb3  30795  cdlemg4f  30804  cdlemg9a  30821  cdlemg9b  30822  cdlemg9  30823  cdlemg11aq  30827  cdlemg12a  30832  cdlemg12b  30833  cdlemg12c  30834  cdlemg12d  30835  cdlemg12f  30837  cdlemg12g  30838  cdlemg12  30839  cdlemg13a  30840  cdlemg16  30846  cdlemg17e  30854  cdlemg17f  30855  cdlemg17g  30856  cdlemg17ir  30859  cdlemg17  30866  cdlemg18b  30868  cdlemg18c  30869  cdlemg33e  30899  trlcoabs2N  30911  trlcocnvat  30913  trlcolem  30915  trlco  30916  cdlemg44  30922  cdlemg47  30925  ltrncom  30927  tendococl  30961  tendoplcl  30970  tendoplcom  30971  tendoplass  30972  tendodi1  30973  tendodi2  30974  tendo0pl  30980  tendoipl  30986  cdlemh1  31004  cdlemi2  31008  tendo0mul  31015  tendo0mulr  31016  cdlemk2  31021  cdlemk3  31022  cdlemk4  31023  cdlemk6  31026  cdlemk8  31027  cdlemk12  31039  cdlemkole  31042  cdlemk14  31043  cdlemk15  31044  cdlemk5u  31050  cdlemk6u  31051  cdlemk12u  31061  cdlemkfid1N  31110  cdlemk19x  31132  cdlemk48  31139  cdlemk53a  31144  cdlemk56  31160  cdleml2N  31166  cdleml3N  31167  cdleml6  31170  cdleml7  31171  dva1dim  31174  dia2dimlem4  31257  dvhlveclem  31298  doca2N  31316  djajN  31327  cdlemn2a  31386  cdlemn3  31387  dihordlem6  31403  dihord5apre  31452  dihglbcpreN  31490  dihmeetcN  31492  dihmeetbN  31493  dihmeetlem10N  31506  dihmeetlem12N  31508  dihmeetlem15N  31511  dihmeetALTN  31517  dih1dimatlem0  31518  dihjatcclem3  31610  dihjatcclem4  31611  mapdpglem22  31883  hdmap14lem1a  32059
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