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

Theorem syl112anc 1186
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 518 . 2  |-  ( ph  ->  ( th  /\  ta ) )
6 syl112anc.5 . 2  |-  ( ( ps  /\  ch  /\  ( th  /\  ta )
)  ->  et )
71, 2, 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:  fveqf1o  5806  gruina  8440  grur1  8442  enqeq  8558  recrec  9457  rec11r  9459  divdivdiv  9461  dmdcan  9470  ddcan  9474  rereccl  9478  div2neg  9483  divmuld  9558  divmul2d  9569  divmul3d  9570  divassd  9571  div12d  9572  div23d  9573  divdird  9574  divsubdird  9575  div11d  9576  ltmul12a  9612  ltdiv1  9620  ltrec  9637  lt2msq1  9639  lediv2  9646  supmul1  9719  qbtwnre  10526  xlemul1a  10608  xlemul1  10610  quoremz  10959  quoremnn0ALT  10961  expgt1  11140  nnlesq  11206  expnbnd  11230  expmulnbnd  11233  discr1  11237  facubnd  11313  hashf1lem1  11393  sqrlem6  11733  mulcn2  12069  climcnds  12310  geomulcvg  12332  cvgrat  12339  eftlub  12389  eflegeo  12401  tanhlt1  12440  sin01bnd  12465  cos01bnd  12466  eirrlem  12482  bitsmod  12627  mulgcd  12725  prmind2  12769  mulgcddvds  12783  qnumgt0  12821  iserodd  12888  pcpremul  12896  fldivp1  12945  pcfaclem  12946  qexpz  12949  prmpwdvds  12951  pockthg  12953  prmreclem1  12963  prmreclem5  12967  4sqlem10  12994  4sqlem12  13003  4sqlem16  13007  4sqlem17  13008  vdwlem3  13030  vdwlem8  13035  vdwlem9  13036  0ram  13067  ramz2  13071  xpsc0  13462  xpsc1  13463  odmulg  14869  dfod2  14877  odf1o1  14883  odf1o2  14884  sylow3lem4  14941  ablsub4  15114  odadd1  15140  odadd2  15141  ablfacrp2  15302  ablfac1b  15305  ablfac1eu  15308  pgpfac1lem3a  15311  pgpfaclem2  15317  chrcong  16483  znrrg  16519  cygznlem1  16520  txdis  17326  txdis1cn  17329  ptunhmeo  17499  divstgplem  17803  blcld  18051  nlmvscnlem2  18196  blcvx  18304  metds0  18354  metdseq0  18358  icopnfcnv  18440  lebnumii  18464  ipcau2  18664  tchcphlem1  18665  ipcnlem2  18671  dyadf  18946  dyadovol  18948  dyaddisjlem  18950  dyadmaxlem  18952  opnmbllem  18956  mbfmulc2lem  19002  mbfi1fseqlem4  19073  mbfi1fseqlem5  19074  mbfi1fseqlem6  19075  itg2mulclem  19101  itg2monolem1  19105  itg2monolem3  19107  itg2cnlem2  19117  itgabs  19189  dvlip  19340  dvlt0  19352  dvcvx  19367  ftc1lem4  19386  dgrcolem2  19655  aaliou3lem2  19723  aaliou3lem9  19730  itgulm  19784  radcnvlem1  19789  abelthlem2  19808  abelthlem7  19814  tangtx  19873  cosne0  19892  cosordlem  19893  tanord1  19899  logdivlti  19971  logcnlem4  19992  logf1o2  19997  cxpcn3lem  20087  cxpaddle  20092  ang180lem2  20108  atanlogsublem  20211  atantan  20219  atanbndlem  20221  atans2  20227  leibpi  20238  log2tlbnd  20241  birthdaylem3  20248  efrlim  20264  jensenlem2  20282  ftalem1  20310  ftalem5  20314  basellem1  20318  basellem4  20321  fsumdvdsdiaglem  20423  dvdsflf1o  20427  fsumfldivdiaglem  20429  ppiub  20443  mersenne  20466  dchrptlem1  20503  bposlem1  20523  bposlem2  20524  bposlem4  20526  lgsdilem  20561  lgseisenlem1  20588  lgseisenlem2  20589  lgseisenlem3  20590  lgsquadlem1  20593  lgsquadlem2  20594  2sqlem3  20605  2sqlem8  20611  2sqlem11  20614  2sqblem  20616  chebbnd1lem2  20619  chebbnd1lem3  20620  rplogsumlem1  20633  rplogsumlem2  20634  dchrisumlem1  20638  dchrmusum2  20643  dchrisum0flblem1  20657  mulog2sumlem1  20683  logdivbnd  20705  pntpbnd1a  20734  pntpbnd1  20735  pntpbnd2  20736  pntlemh  20748  pntlemr  20751  pntlemk  20755  pntlemo  20756  ostth2lem1  20767  ostth2lem2  20783  ostth2lem3  20784  ostth3  20787  gxmodid  20946  nmbdoplbi  22604  nmcoplbi  22608  nmophmi  22611  nmbdfnlbi  22629  nmcfnlbi  22632  cnlnadjlem7  22653  nmopcoi  22675  zetacvg  23100  subfaclim  23130  conpcon  23177  cvmliftlem2  23228  cvmliftlem6  23232  cvmliftlem7  23233  cvmliftlem8  23234  cvmliftlem9  23235  cvmliftlem10  23236  vdgrun  23304  eupath2lem3  23314  snmlff  23323  axsegcon  23966  axpaschlem  23979  lineext  24110  hilbert1.1  24188  muldisc  24893  limptlimpr2lem1  24986  altretop  25012  cntrset  25014  tcnvec  25102  nn0prpwlem  25650  csbrn  25874  trirn  25875  bfplem1  25958  bfp  25960  eldioph2lem1  26251  fphpdo  26312  irrapxlem1  26319  irrapxlem2  26320  irrapxlem3  26321  irrapxlem5  26323  pellexlem2  26327  pell1234qrreccl  26351  pell1234qrmulcl  26352  pell1234qrdich  26358  pell1qr1  26368  pellqrexplicit  26374  pellfundex  26383  reglogltb  26388  reglogleb  26389  pellfund14  26395  rmspecsqrnq  26403  rmxycomplete  26414  jm2.24nn  26458  jm2.17b  26460  jm2.17c  26461  jm2.18  26493  jm2.19lem2  26495  jm2.20nn  26502  jm2.16nn0  26509  jm3.1lem2  26523  enfixsn  26669  lfl1  28633  lfladdcl  28634  eqlkr  28662  lkrlsp  28665  atcvrj2b  28994  3dim1  29029  3dim2  29030  llni2  29074  2llnjaN  29128  lvoli3  29139  lvoli2  29143  lncvrelatN  29343  lhpat4N  29606  lhpat3  29608  4atexlemex6  29636  ldilco  29678  ltrnid  29697  ltrnatb  29699  ltrnel  29701  ltrncnvel  29704  ltrncnv  29708  ltrn11at  29709  ltrneq  29711  ltrnmw  29713  trlat  29731  trlator0  29733  ltrnnidn  29736  trlid0  29738  trlnidatb  29739  trlnle  29748  trlval3  29749  trlval4  29750  cdlemc2  29754  cdlemc5  29757  cdlemc6  29758  cdlemc  29759  cdlemd2  29761  cdlemd9  29768  cdleme0e  29779  cdleme02N  29784  cdleme0ex1N  29785  cdleme3e  29794  cdleme3g  29796  cdleme3h  29797  cdleme3  29799  cdleme7aa  29804  cdleme7b  29806  cdleme7c  29807  cdleme7d  29808  cdleme7e  29809  cdleme7ga  29810  cdleme7  29811  cdleme9  29815  cdleme16aN  29821  cdleme11c  29823  cdleme11dN  29824  cdleme11e  29825  cdleme11h  29828  cdleme11j  29829  cdleme11k  29830  cdleme12  29833  cdleme21j  29898  cdleme26eALTN  29923  cdleme26f  29925  cdleme26f2  29927  cdlemefrs29bpre0  29958  cdleme35a  30010  cdleme35b  30012  cdleme35c  30013  cdleme35f  30016  cdleme36a  30022  cdleme38m  30025  cdlemeg46rgv  30090  cdlemeg46req  30091  cdlemf  30125  cdlemg2fvlem  30156  cdlemg2l  30165  cdlemg7N  30188  cdlemg12g  30211  cdlemg15  30218  cdlemg17h  30230  cdlemg17  30239  cdlemg19a  30245  cdlemg24  30250  cdlemg37  30251  cdlemg27a  30254  cdlemg31b0N  30256  cdlemg27b  30258  cdlemg31c  30261  cdlemg31d  30262  cdlemg35  30275  trljco  30302  tgrpgrplem  30311  cdlemh2  30378  tendoconid  30391  tendotr  30392  cdlemk35s-id  30500  cdlemk39s-id  30502  cdlemk53b  30518  cdlemk53  30519  cdlemk54  30520  cdleml3N  30540  cdleml5N  30542  tendospcanN  30586  diclss  30756  dihvalcq2  30810  dihord4  30821  dihord5b  30822  dihord5apre  30825  dihmeetlem1N  30853  dihmeetbclemN  30867  dihmeetlem20N  30889  dihmeetALTN  30890  dihatlat  30897  dihatexv  30901  dochkr1  31041  dochkr1OLDN  31042  lcfl7lem  31062  lclkrlem2m  31082  hdmaplna1  31473  hdmaplns1  31474  hdmaplnm1  31475
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