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

Theorem syl121anc 1190
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 520 . 2  |-  ( ph  ->  ( ch  /\  th ) )
5 sylXanc.4 . 2  |-  ( ph  ->  ta )
6 syl121anc.5 . 2  |-  ( ( ps  /\  ( ch 
/\  th )  /\  ta )  ->  et )
71, 4, 5, 6syl3anc 1185 1  |-  ( ph  ->  et )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  syl122anc  1194  disjxiun  4240  tfisi  4873  fsnunf2  5968  axdc4lem  8373  div32d  9851  div13d  9852  expdivd  11575  pcqmul  13265  pcid  13284  pcneg  13285  pc2dvds  13290  pcz  13292  pcaddlem  13295  pcadd  13296  pcmpt2  13300  pcbc  13307  qexpz  13308  expnprm  13309  spwpr4c  14702  sylow1lem1  15270  lspsneleq  16225  lspsneq  16232  lspfixed  16238  ucncn  18353  ucnextcn  18372  ssblex  18496  prdsxmslem2  18597  voliunlem1  19482  deg1mul3le  20077  deg1pw  20081  fta1blem  20129  bcmono  21099  dchrisum0flblem1  21240  dchrisum0flblem2  21241  pntibndlem1  21321  pntlemr  21334  0wlkon  21585  0pthon  21617  nv1  22203  measun  24600  measvuni  24603  measunl  24605  btwnconn1lem14  26069  segcon2  26074  seglelin  26085  neibastop3  26433  upixp  26473  fdc  26491  eldioph2b  26933  jm2.19lem4  27175  jm2.19  27176  jm2.26a  27183  jm2.26  27185  hbtlem2  27417  fnchoice  27788  stoweidlem42  27879  stoweidlem59  27896  eqlkr3  30073  lkrshp  30077  lfl1dim  30093  lfl1dim2N  30094  eqlkr4  30137  2llnneN  30380  3dim2  30439  4atlem3  30567  4atlem11  30580  4atlem12  30583  pexmidlem4N  30944  lhp2at0nle  31006  lhple  31013  ltrnideq  31146  cdlemd9  31177  cdleme0ex2N  31195  cdleme0moN  31196  cdleme11a  31231  cdleme30a  31349  cdlemefs32sn1aw  31385  cdleme43fsv1snlem  31391  cdlemefs31fv1  31395  cdlemefs45eN  31402  cdleme41sn3a  31404  cdleme35h  31427  cdleme36a  31431  cdleme40m  31438  cdleme40n  31439  cdleme41sn3aw  31445  cdleme42h  31453  cdleme42k  31455  cdleme42mN  31458  cdleme43cN  31462  cdleme17d3  31467  cdleme48fvg  31471  cdlemeg47rv2  31481  cdlemeg46c  31484  cdlemeg46sfg  31491  cdlemeg46rjgN  31493  cdlemeg46rgv  31499  cdlemeg46req  31500  cdlemeg46gfv  31501  cdlemeg46gfre  31503  cdlemeg49lebilem  31510  cdleme50trn2  31522  cdlemg2kq  31573  cdlemb3  31577  cdlemg4f  31586  cdlemg9a  31603  cdlemg9b  31604  cdlemg9  31605  cdlemg11aq  31609  cdlemg12a  31614  cdlemg12b  31615  cdlemg12c  31616  cdlemg12d  31617  cdlemg12f  31619  cdlemg12g  31620  cdlemg12  31621  cdlemg13a  31622  cdlemg16  31628  cdlemg17e  31636  cdlemg17f  31637  cdlemg17g  31638  cdlemg17ir  31641  cdlemg17  31648  cdlemg18b  31650  cdlemg18c  31651  cdlemg33e  31681  trlcoabs2N  31693  trlcocnvat  31695  trlcolem  31697  trlco  31698  cdlemg44  31704  cdlemg47  31707  ltrncom  31709  tendococl  31743  tendoplcl  31752  tendoplcom  31753  tendoplass  31754  tendodi1  31755  tendodi2  31756  tendo0pl  31762  tendoipl  31768  cdlemh1  31786  cdlemi2  31790  tendo0mul  31797  tendo0mulr  31798  cdlemk2  31803  cdlemk3  31804  cdlemk4  31805  cdlemk6  31808  cdlemk8  31809  cdlemk12  31821  cdlemkole  31824  cdlemk14  31825  cdlemk15  31826  cdlemk5u  31832  cdlemk6u  31833  cdlemk12u  31843  cdlemkfid1N  31892  cdlemk19x  31914  cdlemk48  31921  cdlemk53a  31926  cdlemk56  31942  cdleml2N  31948  cdleml3N  31949  cdleml6  31952  cdleml7  31953  dva1dim  31956  dia2dimlem4  32039  dvhlveclem  32080  doca2N  32098  djajN  32109  cdlemn2a  32168  cdlemn3  32169  dihordlem6  32185  dihord5apre  32234  dihglbcpreN  32272  dihmeetcN  32274  dihmeetbN  32275  dihmeetlem10N  32288  dihmeetlem12N  32290  dihmeetlem15N  32293  dihmeetALTN  32299  dih1dimatlem0  32300  dihjatcclem3  32392  dihjatcclem4  32393  mapdpglem22  32665  hdmap14lem1a  32841
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator