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

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

Proof of Theorem syl112anc
StepHypRef Expression
1 sylXanc.1 . 2  |-  ( ph  ->  ps )
2 sylXanc.2 . 2  |-  ( ph  ->  ch )
3 sylXanc.3 . . 3  |-  ( ph  ->  th )
4 sylXanc.4 . . 3  |-  ( ph  ->  ta )
53, 4jca 519 . 2  |-  ( ph  ->  ( th  /\  ta ) )
6 syl112anc.5 . 2  |-  ( ( ps  /\  ch  /\  ( th  /\  ta )
)  ->  et )
71, 2, 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:  fveqf1o  6020  gruina  8682  grur1  8684  enqeq  8800  recrec  9700  rec11r  9702  divdivdiv  9704  dmdcan  9713  ddcan  9717  rereccl  9721  div2neg  9726  divmuld  9801  divmul2d  9812  divmul3d  9813  divassd  9814  div12d  9815  div23d  9816  divdird  9817  divsubdird  9818  div11d  9819  ltmul12a  9855  ltdiv1  9863  ltrec  9880  lt2msq1  9882  lediv2  9889  supmul1  9962  qbtwnre  10774  xlemul1a  10856  xlemul1  10858  xadd4d  10871  quoremz  11224  quoremnn0ALT  11226  expgt1  11406  nnlesq  11472  expnbnd  11496  expmulnbnd  11499  discr1  11503  facubnd  11579  hashf1lem1  11692  sqrlem6  12041  mulcn2  12377  climcnds  12619  geomulcvg  12641  cvgrat  12648  eftlub  12698  eflegeo  12710  tanhlt1  12749  sin01bnd  12774  cos01bnd  12775  eirrlem  12791  bitsmod  12936  mulgcd  13034  prmind2  13078  mulgcddvds  13092  qnumgt0  13130  iserodd  13197  pcpremul  13205  fldivp1  13254  pcfaclem  13255  qexpz  13258  prmpwdvds  13260  pockthg  13262  prmreclem1  13272  prmreclem5  13276  4sqlem10  13303  4sqlem12  13312  4sqlem16  13316  4sqlem17  13317  vdwlem3  13339  vdwlem8  13344  vdwlem9  13345  0ram  13376  ramz2  13380  xpsc0  13773  xpsc1  13774  odmulg  15180  dfod2  15188  odf1o1  15194  odf1o2  15195  sylow3lem4  15252  ablsub4  15425  odadd1  15451  odadd2  15452  ablfacrp2  15613  ablfac1b  15616  ablfac1eu  15619  pgpfac1lem3a  15622  pgpfaclem2  15628  chrcong  16798  znrrg  16834  cygznlem1  16835  txdis  17652  txdis1cn  17655  ptunhmeo  17828  divstgplem  18138  blcld  18523  nlmvscnlem2  18709  blcvx  18817  metds0  18868  metdseq0  18872  icopnfcnv  18955  lebnumii  18979  ipcau2  19179  tchcphlem1  19180  ipcnlem2  19186  dyadf  19471  dyadovol  19473  dyaddisjlem  19475  dyadmaxlem  19477  opnmbllem  19481  mbfmulc2lem  19527  mbfi1fseqlem4  19598  mbfi1fseqlem5  19599  mbfi1fseqlem6  19600  itg2mulclem  19626  itg2monolem1  19630  itg2monolem3  19632  itg2cnlem2  19642  itgabs  19714  dvlip  19865  dvlt0  19877  dvcvx  19892  ftc1lem4  19911  dgrcolem2  20180  aaliou3lem2  20248  aaliou3lem9  20255  itgulm  20312  radcnvlem1  20317  abelthlem2  20336  abelthlem7  20342  tangtx  20401  cosne0  20420  cosordlem  20421  tanord1  20427  logdivlti  20503  logcnlem4  20524  logf1o2  20529  cxpcn3lem  20619  cxpaddle  20624  ang180lem2  20640  atanlogsublem  20743  atantan  20751  atanbndlem  20753  atans2  20759  leibpi  20770  log2tlbnd  20773  birthdaylem3  20780  efrlim  20796  jensenlem2  20814  ftalem1  20843  ftalem5  20847  basellem1  20851  basellem4  20854  fsumdvdsdiaglem  20956  dvdsflf1o  20960  fsumfldivdiaglem  20962  ppiub  20976  mersenne  20999  dchrptlem1  21036  bposlem1  21056  bposlem2  21057  bposlem4  21059  lgsdilem  21094  lgseisenlem1  21121  lgseisenlem2  21122  lgseisenlem3  21123  lgsquadlem1  21126  lgsquadlem2  21127  2sqlem3  21138  2sqlem8  21144  2sqlem11  21147  2sqblem  21149  chebbnd1lem2  21152  chebbnd1lem3  21153  rplogsumlem1  21166  rplogsumlem2  21167  dchrisumlem1  21171  dchrmusum2  21176  dchrisum0flblem1  21190  mulog2sumlem1  21216  logdivbnd  21238  pntpbnd1a  21267  pntpbnd1  21268  pntpbnd2  21269  pntlemh  21281  pntlemr  21284  pntlemk  21288  pntlemo  21289  ostth2lem1  21300  ostth2lem2  21316  ostth2lem3  21317  ostth3  21320  vdgrun  21660  vdgrfiun  21661  eupath2lem3  21689  gxmodid  21855  nmbdoplbi  23515  nmcoplbi  23519  nmophmi  23522  nmbdfnlbi  23540  nmcfnlbi  23543  cnlnadjlem7  23564  nmopcoi  23586  xdivrec  24161  unitdivcld  24287  measvunilem  24554  measvuni  24556  measssd  24557  measiuns  24559  measinblem  24562  measdivcst  24567  probun  24665  totprobd  24672  dstrvprob  24717  zetacvg  24787  subfaclim  24862  conpcon  24910  cvmliftlem2  24961  cvmliftlem6  24965  cvmliftlem7  24966  cvmliftlem8  24967  cvmliftlem9  24968  cvmliftlem10  24969  snmlff  25004  axsegcon  25814  axpaschlem  25827  lineext  25958  hilbert1.1  26036  ismblfin  26193  itgabsnc  26220  ftc1cnnclem  26224  nn0prpwlem  26262  csbrn  26393  trirn  26394  bfplem1  26468  bfp  26470  eldioph2lem1  26755  fphpdo  26815  irrapxlem1  26822  irrapxlem2  26823  irrapxlem3  26824  irrapxlem5  26826  pellexlem2  26830  pell1234qrreccl  26854  pell1234qrmulcl  26855  pell1234qrdich  26861  pell1qr1  26871  pellqrexplicit  26877  pellfundex  26886  reglogltb  26891  reglogleb  26892  pellfund14  26898  rmspecsqrnq  26906  rmxycomplete  26917  jm2.24nn  26961  jm2.17b  26963  jm2.17c  26964  jm2.18  26996  jm2.19lem2  26998  jm2.20nn  27005  jm2.16nn0  27012  jm3.1lem2  27026  enfixsn  27172  stoweidlem1  27664  stoweidlem11  27674  stoweidlem14  27677  stoweidlem26  27689  stoweidlem34  27697  stoweidlem38  27701  stoweidlem60  27723  lfl1  29707  lfladdcl  29708  eqlkr  29736  lkrlsp  29739  atcvrj2b  30068  3dim1  30103  3dim2  30104  llni2  30148  2llnjaN  30202  lvoli3  30213  lvoli2  30217  lncvrelatN  30417  lhpat4N  30680  lhpat3  30682  4atexlemex6  30710  ldilco  30752  ltrnid  30771  ltrnatb  30773  ltrnel  30775  ltrncnvel  30778  ltrncnv  30782  ltrn11at  30783  ltrneq  30785  ltrnmw  30787  trlat  30805  trlator0  30807  ltrnnidn  30810  trlid0  30812  trlnidatb  30813  trlnle  30822  trlval3  30823  trlval4  30824  cdlemc2  30828  cdlemc5  30831  cdlemc6  30832  cdlemc  30833  cdlemd2  30835  cdlemd9  30842  cdleme0e  30853  cdleme02N  30858  cdleme0ex1N  30859  cdleme3e  30868  cdleme3g  30870  cdleme3h  30871  cdleme3  30873  cdleme7aa  30878  cdleme7b  30880  cdleme7c  30881  cdleme7d  30882  cdleme7e  30883  cdleme7ga  30884  cdleme7  30885  cdleme9  30889  cdleme16aN  30895  cdleme11c  30897  cdleme11dN  30898  cdleme11e  30899  cdleme11h  30902  cdleme11j  30903  cdleme11k  30904  cdleme12  30907  cdleme21j  30972  cdleme26eALTN  30997  cdleme26f  30999  cdleme26f2  31001  cdlemefrs29bpre0  31032  cdleme35a  31084  cdleme35b  31086  cdleme35c  31087  cdleme35f  31090  cdleme36a  31096  cdleme38m  31099  cdlemeg46rgv  31164  cdlemeg46req  31165  cdlemf  31199  cdlemg2fvlem  31230  cdlemg2l  31239  cdlemg7N  31262  cdlemg12g  31285  cdlemg15  31292  cdlemg17h  31304  cdlemg17  31313  cdlemg19a  31319  cdlemg24  31324  cdlemg37  31325  cdlemg27a  31328  cdlemg31b0N  31330  cdlemg27b  31332  cdlemg31c  31335  cdlemg31d  31336  cdlemg35  31349  trljco  31376  tgrpgrplem  31385  cdlemh2  31452  tendoconid  31465  tendotr  31466  cdlemk35s-id  31574  cdlemk39s-id  31576  cdlemk53b  31592  cdlemk53  31593  cdlemk54  31594  cdleml3N  31614  cdleml5N  31616  tendospcanN  31660  diclss  31830  dihvalcq2  31884  dihord4  31895  dihord5b  31896  dihord5apre  31899  dihmeetlem1N  31927  dihmeetbclemN  31941  dihmeetlem20N  31963  dihmeetALTN  31964  dihatlat  31971  dihatexv  31975  dochkr1  32115  dochkr1OLDN  32116  lcfl7lem  32136  lclkrlem2m  32156  hdmaplna1  32547  hdmaplns1  32548  hdmaplnm1  32549
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