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  xdivrec  23110  unitdivcld  23285  esumcst  23436  measvunilem  23540  dya2iocseg  23579  probun  23622  zetacvg  23689  subfaclim  23719  conpcon  23766  cvmliftlem2  23817  cvmliftlem6  23821  cvmliftlem7  23822  cvmliftlem8  23823  cvmliftlem9  23824  cvmliftlem10  23825  vdgrun  23893  eupath2lem3  23903  snmlff  23912  axsegcon  24555  axpaschlem  24568  lineext  24699  hilbert1.1  24777  muldisc  25481  limptlimpr2lem1  25574  altretop  25600  cntrset  25602  tcnvec  25690  nn0prpwlem  26238  csbrn  26462  trirn  26463  bfplem1  26546  bfp  26548  eldioph2lem1  26839  fphpdo  26900  irrapxlem1  26907  irrapxlem2  26908  irrapxlem3  26909  irrapxlem5  26911  pellexlem2  26915  pell1234qrreccl  26939  pell1234qrmulcl  26940  pell1234qrdich  26946  pell1qr1  26956  pellqrexplicit  26962  pellfundex  26971  reglogltb  26976  reglogleb  26977  pellfund14  26983  rmspecsqrnq  26991  rmxycomplete  27002  jm2.24nn  27046  jm2.17b  27048  jm2.17c  27049  jm2.18  27081  jm2.19lem2  27083  jm2.20nn  27090  jm2.16nn0  27097  jm3.1lem2  27111  enfixsn  27257  lfl1  29260  lfladdcl  29261  eqlkr  29289  lkrlsp  29292  atcvrj2b  29621  3dim1  29656  3dim2  29657  llni2  29701  2llnjaN  29755  lvoli3  29766  lvoli2  29770  lncvrelatN  29970  lhpat4N  30233  lhpat3  30235  4atexlemex6  30263  ldilco  30305  ltrnid  30324  ltrnatb  30326  ltrnel  30328  ltrncnvel  30331  ltrncnv  30335  ltrn11at  30336  ltrneq  30338  ltrnmw  30340  trlat  30358  trlator0  30360  ltrnnidn  30363  trlid0  30365  trlnidatb  30366  trlnle  30375  trlval3  30376  trlval4  30377  cdlemc2  30381  cdlemc5  30384  cdlemc6  30385  cdlemc  30386  cdlemd2  30388  cdlemd9  30395  cdleme0e  30406  cdleme02N  30411  cdleme0ex1N  30412  cdleme3e  30421  cdleme3g  30423  cdleme3h  30424  cdleme3  30426  cdleme7aa  30431  cdleme7b  30433  cdleme7c  30434  cdleme7d  30435  cdleme7e  30436  cdleme7ga  30437  cdleme7  30438  cdleme9  30442  cdleme16aN  30448  cdleme11c  30450  cdleme11dN  30451  cdleme11e  30452  cdleme11h  30455  cdleme11j  30456  cdleme11k  30457  cdleme12  30460  cdleme21j  30525  cdleme26eALTN  30550  cdleme26f  30552  cdleme26f2  30554  cdlemefrs29bpre0  30585  cdleme35a  30637  cdleme35b  30639  cdleme35c  30640  cdleme35f  30643  cdleme36a  30649  cdleme38m  30652  cdlemeg46rgv  30717  cdlemeg46req  30718  cdlemf  30752  cdlemg2fvlem  30783  cdlemg2l  30792  cdlemg7N  30815  cdlemg12g  30838  cdlemg15  30845  cdlemg17h  30857  cdlemg17  30866  cdlemg19a  30872  cdlemg24  30877  cdlemg37  30878  cdlemg27a  30881  cdlemg31b0N  30883  cdlemg27b  30885  cdlemg31c  30888  cdlemg31d  30889  cdlemg35  30902  trljco  30929  tgrpgrplem  30938  cdlemh2  31005  tendoconid  31018  tendotr  31019  cdlemk35s-id  31127  cdlemk39s-id  31129  cdlemk53b  31145  cdlemk53  31146  cdlemk54  31147  cdleml3N  31167  cdleml5N  31169  tendospcanN  31213  diclss  31383  dihvalcq2  31437  dihord4  31448  dihord5b  31449  dihord5apre  31452  dihmeetlem1N  31480  dihmeetbclemN  31494  dihmeetlem20N  31516  dihmeetALTN  31517  dihatlat  31524  dihatexv  31528  dochkr1  31668  dochkr1OLDN  31669  lcfl7lem  31689  lclkrlem2m  31709  hdmaplna1  32100  hdmaplns1  32101  hdmaplnm1  32102
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