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

Theorem syl112anc 1215
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 529 . 2  |-  ( ph  ->  ( th  /\  ta ) )
6 syl112anc.5 . 2  |-  ( ( ps  /\  ch  /\  ( th  /\  ta )
)  ->  et )
71, 2, 5, 6syl3anc 1211 1  |-  ( ph  ->  et )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 958
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 185  df-an 371  df-3an 960
This theorem is referenced by:  fveqf1o  5987  enfixsn  7408  gruina  8973  grur1  8975  enqeq  9091  recrec  10016  rec11r  10018  divdivdiv  10020  dmdcan  10029  ddcan  10033  rereccl  10037  div2neg  10042  divmuld  10117  divmul2d  10128  divmul3d  10129  divassd  10130  div12d  10131  div23d  10132  divdird  10133  divsubdird  10134  div11d  10135  ltmul12a  10173  ltdiv1  10181  ltrec  10201  lt2msq1  10203  lediv2  10210  supmul1  10283  qbtwnre  11157  xlemul1a  11239  xlemul1  11241  xadd4d  11254  quoremz  11678  quoremnn0ALT  11680  expgt1  11886  nnlesq  11953  expnbnd  11977  expmulnbnd  11980  discr1  11984  facubnd  12060  hashf1lem1  12192  2swrdeqwrdeq  12331  sqrlem6  12721  mulcn2  13057  climcnds  13297  geomulcvg  13319  cvgrat  13326  eftlub  13376  eflegeo  13388  tanhlt1  13427  sin01bnd  13452  cos01bnd  13453  eirrlem  13469  bitsmod  13615  mulgcd  13713  prmind2  13757  mulgcddvds  13773  qnumgt0  13811  iserodd  13885  pcpremul  13893  fldivp1  13942  pcfaclem  13943  qexpz  13946  prmpwdvds  13948  pockthg  13950  prmreclem1  13960  prmreclem5  13964  4sqlem10  13991  4sqlem12  14000  4sqlem16  14004  4sqlem17  14005  vdwlem3  14027  vdwlem8  14032  vdwlem9  14033  0ram  14064  ramz2  14068  xpsc0  14481  xpsc1  14482  odmulg  16037  dfod2  16045  odf1o1  16051  odf1o2  16052  sylow3lem4  16109  ablsub4  16282  odadd1  16310  odadd2  16311  ablfacrp2  16542  ablfac1b  16545  ablfac1eu  16548  pgpfac1lem3a  16551  pgpfaclem2  16557  chrcong  17802  znrrg  17840  cygznlem1  17841  txdis  19047  txdis1cn  19050  ptunhmeo  19223  divstgplem  19533  blcld  19922  nlmvscnlem2  20108  blcvx  20217  metds0  20268  metdseq0  20272  icopnfcnv  20356  lebnumii  20380  ipcau2  20591  tchcphlem1  20592  ipcnlem2  20598  csbren  20740  trirn  20741  dyadf  20913  dyadovol  20915  dyaddisjlem  20917  dyadmaxlem  20919  opnmbllem  20923  mbfmulc2lem  20967  mbfi1fseqlem4  21038  mbfi1fseqlem5  21039  mbfi1fseqlem6  21040  itg2mulclem  21066  itg2monolem1  21070  itg2monolem3  21072  itg2cnlem2  21082  itgabs  21154  dvlip  21307  dvlt0  21319  dvcvx  21334  ftc1lem4  21353  dgrcolem2  21626  aaliou3lem2  21694  aaliou3lem9  21701  itgulm  21758  radcnvlem1  21763  abelthlem2  21782  abelthlem7  21788  tangtx  21852  cosne0  21871  cosordlem  21872  tanord1  21878  logdivlti  21954  logcnlem4  21975  logf1o2  21980  cxpcn3lem  22070  cxpaddle  22075  ang180lem2  22091  atanlogsublem  22195  atantan  22203  atanbndlem  22205  atans2  22211  leibpi  22222  log2tlbnd  22225  birthdaylem3  22232  efrlim  22248  jensenlem2  22266  ftalem1  22295  ftalem5  22299  basellem1  22303  basellem4  22306  fsumdvdsdiaglem  22408  dvdsflf1o  22412  fsumfldivdiaglem  22414  ppiub  22428  mersenne  22451  dchrptlem1  22488  bposlem1  22508  bposlem2  22509  bposlem4  22511  lgsdilem  22546  lgseisenlem1  22573  lgseisenlem2  22574  lgseisenlem3  22575  lgsquadlem1  22578  lgsquadlem2  22579  2sqlem3  22590  2sqlem8  22596  2sqlem11  22599  2sqblem  22601  chebbnd1lem2  22604  chebbnd1lem3  22605  rplogsumlem1  22618  rplogsumlem2  22619  dchrisumlem1  22623  dchrmusum2  22628  dchrisum0flblem1  22642  mulog2sumlem1  22668  logdivbnd  22690  pntpbnd1a  22719  pntpbnd1  22720  pntpbnd2  22721  pntlemh  22733  pntlemr  22736  pntlemk  22740  pntlemo  22741  ostth2lem1  22752  ostth2lem2  22768  ostth2lem3  22769  ostth3  22772  axsegcon  22996  axpaschlem  23009  vdgrun  23394  vdgrfiun  23395  eupath2lem3  23423  gxmodid  23589  nmbdoplbi  25251  nmcoplbi  25255  nmophmi  25258  nmbdfnlbi  25276  nmcfnlbi  25279  cnlnadjlem7  25300  nmopcoi  25322  resf1o  25855  xdivrec  25925  unitdivcld  26185  measvunilem  26480  measvuni  26482  measssd  26483  measiuns  26485  measinblem  26488  measdivcst  26493  oddpwdc  26585  probun  26650  totprobd  26657  dstrvprob  26702  zetacvg  26849  subfaclim  26924  conpcon  26972  cvmliftlem2  27023  cvmliftlem6  27027  cvmliftlem7  27028  cvmliftlem8  27029  cvmliftlem9  27030  cvmliftlem10  27031  snmlff  27066  lineext  27954  hilbert1.1  28032  opnmbllem0  28271  ismblfin  28276  itgabsnc  28305  ftc1cnnclem  28309  nn0prpwlem  28361  bfplem1  28565  bfp  28567  eldioph2lem1  28943  fphpdo  29001  irrapxlem1  29008  irrapxlem2  29009  irrapxlem3  29010  irrapxlem5  29012  pellexlem2  29016  pell1234qrreccl  29040  pell1234qrmulcl  29041  pell1234qrdich  29047  pell1qr1  29057  pellqrexplicit  29063  pellfundex  29072  reglogltb  29077  reglogleb  29078  pellfund14  29084  rmspecsqrnq  29092  rmxycomplete  29103  jm2.24nn  29147  jm2.17b  29149  jm2.17c  29150  jm2.18  29182  jm2.19lem2  29184  jm2.20nn  29191  jm2.16nn0  29198  jm3.1lem2  29212  stoweidlem1  29642  stoweidlem11  29652  stoweidlem14  29655  stoweidlem26  29667  stoweidlem34  29675  stoweidlem38  29679  stoweidlem60  29701  clwwlkf1  30304  domnmsuppn0  30613  lincvalpr  30661  ldepspr  30716  islindeps2  30726  lfl1  32288  lfladdcl  32289  eqlkr  32317  lkrlsp  32320  atcvrj2b  32649  3dim1  32684  3dim2  32685  llni2  32729  2llnjaN  32783  lvoli3  32794  lvoli2  32798  lncvrelatN  32998  lhpat4N  33261  lhpat3  33263  4atexlemex6  33291  ldilco  33333  ltrnid  33352  ltrnatb  33354  ltrnel  33356  ltrncnvel  33359  ltrncnv  33363  ltrn11at  33364  ltrneq  33366  ltrnmw  33368  trlat  33386  trlator0  33388  ltrnnidn  33391  trlid0  33393  trlnidatb  33394  trlnle  33403  trlval3  33404  trlval4  33405  cdlemc2  33409  cdlemc5  33412  cdlemc6  33413  cdlemc  33414  cdlemd2  33416  cdlemd9  33423  cdleme0e  33434  cdleme02N  33439  cdleme0ex1N  33440  cdleme3e  33449  cdleme3g  33451  cdleme3h  33452  cdleme3  33454  cdleme7aa  33459  cdleme7b  33461  cdleme7c  33462  cdleme7d  33463  cdleme7e  33464  cdleme7ga  33465  cdleme7  33466  cdleme9  33470  cdleme16aN  33476  cdleme11c  33478  cdleme11dN  33479  cdleme11e  33480  cdleme11h  33483  cdleme11j  33484  cdleme11k  33485  cdleme12  33488  cdleme21j  33553  cdleme26eALTN  33578  cdleme26f  33580  cdleme26f2  33582  cdlemefrs29bpre0  33613  cdleme35a  33665  cdleme35b  33667  cdleme35c  33668  cdleme35f  33671  cdleme36a  33677  cdleme38m  33680  cdlemeg46rgv  33745  cdlemeg46req  33746  cdlemf  33780  cdlemg2fvlem  33811  cdlemg2l  33820  cdlemg7N  33843  cdlemg12g  33866  cdlemg15  33873  cdlemg17h  33885  cdlemg17  33894  cdlemg19a  33900  cdlemg24  33905  cdlemg37  33906  cdlemg27a  33909  cdlemg31b0N  33911  cdlemg27b  33913  cdlemg31c  33916  cdlemg31d  33917  cdlemg35  33930  trljco  33957  tgrpgrplem  33966  cdlemh2  34033  tendoconid  34046  tendotr  34047  cdlemk35s-id  34155  cdlemk39s-id  34157  cdlemk53b  34173  cdlemk53  34174  cdlemk54  34175  cdleml3N  34195  cdleml5N  34197  tendospcanN  34241  diclss  34411  dihvalcq2  34465  dihord4  34476  dihord5b  34477  dihord5apre  34480  dihmeetlem1N  34508  dihmeetbclemN  34522  dihmeetlem20N  34544  dihmeetALTN  34545  dihatlat  34552  dihatexv  34556  dochkr1  34696  dochkr1OLDN  34697  lcfl7lem  34717  lclkrlem2m  34737  hdmaplna1  35128  hdmaplns1  35129  hdmaplnm1  35130
  Copyright terms: Public domain W3C validator