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

Theorem syl121anc 1189
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 519 . 2  |-  ( ph  ->  ( ch  /\  th ) )
5 sylXanc.4 . 2  |-  ( ph  ->  ta )
6 syl121anc.5 . 2  |-  ( ( ps  /\  ( ch 
/\  th )  /\  ta )  ->  et )
71, 4, 5, 6syl3anc 1184 1  |-  ( ph  ->  et )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  syl122anc  1193  disjxiun  4201  tfisi  4829  fsnunf2  5923  axdc4lem  8324  div32d  9802  div13d  9803  expdivd  11525  pcqmul  13215  pcid  13234  pcneg  13235  pc2dvds  13240  pcz  13242  pcaddlem  13245  pcadd  13246  pcmpt2  13250  pcbc  13257  qexpz  13258  expnprm  13259  spwpr4c  14652  sylow1lem1  15220  lspsneleq  16175  lspsneq  16182  lspfixed  16188  ucncn  18303  ucnextcn  18322  ssblex  18446  prdsxmslem2  18547  voliunlem1  19432  deg1mul3le  20027  deg1pw  20031  fta1blem  20079  bcmono  21049  dchrisum0flblem1  21190  dchrisum0flblem2  21191  pntibndlem1  21271  pntlemr  21284  0wlkon  21535  0pthon  21567  nv1  22153  measun  24553  measvuni  24556  measunl  24558  btwnconn1lem14  25982  segcon2  25987  seglelin  25998  neibastop3  26328  upixp  26368  fdc  26386  eldioph2b  26758  jm2.19lem4  27000  jm2.19  27001  jm2.26a  27008  jm2.26  27010  hbtlem2  27243  fnchoice  27614  stoweidlem42  27705  stoweidlem59  27722  eqlkr3  29738  lkrshp  29742  lfl1dim  29758  lfl1dim2N  29759  eqlkr4  29802  2llnneN  30045  3dim2  30104  4atlem3  30232  4atlem11  30245  4atlem12  30248  pexmidlem4N  30609  lhp2at0nle  30671  lhple  30678  ltrnideq  30811  cdlemd9  30842  cdleme0ex2N  30860  cdleme0moN  30861  cdleme11a  30896  cdleme30a  31014  cdlemefs32sn1aw  31050  cdleme43fsv1snlem  31056  cdlemefs31fv1  31060  cdlemefs45eN  31067  cdleme41sn3a  31069  cdleme35h  31092  cdleme36a  31096  cdleme40m  31103  cdleme40n  31104  cdleme41sn3aw  31110  cdleme42h  31118  cdleme42k  31120  cdleme42mN  31123  cdleme43cN  31127  cdleme17d3  31132  cdleme48fvg  31136  cdlemeg47rv2  31146  cdlemeg46c  31149  cdlemeg46sfg  31156  cdlemeg46rjgN  31158  cdlemeg46rgv  31164  cdlemeg46req  31165  cdlemeg46gfv  31166  cdlemeg46gfre  31168  cdlemeg49lebilem  31175  cdleme50trn2  31187  cdlemg2kq  31238  cdlemb3  31242  cdlemg4f  31251  cdlemg9a  31268  cdlemg9b  31269  cdlemg9  31270  cdlemg11aq  31274  cdlemg12a  31279  cdlemg12b  31280  cdlemg12c  31281  cdlemg12d  31282  cdlemg12f  31284  cdlemg12g  31285  cdlemg12  31286  cdlemg13a  31287  cdlemg16  31293  cdlemg17e  31301  cdlemg17f  31302  cdlemg17g  31303  cdlemg17ir  31306  cdlemg17  31313  cdlemg18b  31315  cdlemg18c  31316  cdlemg33e  31346  trlcoabs2N  31358  trlcocnvat  31360  trlcolem  31362  trlco  31363  cdlemg44  31369  cdlemg47  31372  ltrncom  31374  tendococl  31408  tendoplcl  31417  tendoplcom  31418  tendoplass  31419  tendodi1  31420  tendodi2  31421  tendo0pl  31427  tendoipl  31433  cdlemh1  31451  cdlemi2  31455  tendo0mul  31462  tendo0mulr  31463  cdlemk2  31468  cdlemk3  31469  cdlemk4  31470  cdlemk6  31473  cdlemk8  31474  cdlemk12  31486  cdlemkole  31489  cdlemk14  31490  cdlemk15  31491  cdlemk5u  31497  cdlemk6u  31498  cdlemk12u  31508  cdlemkfid1N  31557  cdlemk19x  31579  cdlemk48  31586  cdlemk53a  31591  cdlemk56  31607  cdleml2N  31613  cdleml3N  31614  cdleml6  31617  cdleml7  31618  dva1dim  31621  dia2dimlem4  31704  dvhlveclem  31745  doca2N  31763  djajN  31774  cdlemn2a  31833  cdlemn3  31834  dihordlem6  31850  dihord5apre  31899  dihglbcpreN  31937  dihmeetcN  31939  dihmeetbN  31940  dihmeetlem10N  31953  dihmeetlem12N  31955  dihmeetlem15N  31958  dihmeetALTN  31964  dih1dimatlem0  31965  dihjatcclem3  32057  dihjatcclem4  32058  mapdpglem22  32330  hdmap14lem1a  32506
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