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

Theorem syl112anc 1223
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 532 . 2  |-  ( ph  ->  ( th  /\  ta ) )
6 syl112anc.5 . 2  |-  ( ( ps  /\  ch  /\  ( th  /\  ta )
)  ->  et )
71, 2, 5, 6syl3anc 1219 1  |-  ( ph  ->  et )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 967
This theorem is referenced by:  fveqf1o  6110  enfixsn  7531  gruina  9097  grur1  9099  enqeq  9215  recrec  10140  rec11r  10142  divdivdiv  10144  dmdcan  10153  ddcan  10157  rereccl  10161  div2neg  10166  divmuld  10241  divmul2d  10252  divmul3d  10253  divassd  10254  div12d  10255  div23d  10256  divdird  10257  divsubdird  10258  div11d  10259  ltmul12a  10297  ltdiv1  10305  ltrec  10325  lt2msq1  10327  lediv2  10334  supmul1  10407  qbtwnre  11281  xlemul1a  11363  xlemul1  11365  xadd4d  11378  quoremz  11812  quoremnn0ALT  11814  expgt1  12020  nnlesq  12087  expnbnd  12111  expmulnbnd  12114  discr1  12118  facubnd  12194  hashf1lem1  12327  2swrdeqwrdeq  12466  sqrlem6  12856  mulcn2  13192  climcnds  13433  geomulcvg  13455  cvgrat  13462  eftlub  13512  eflegeo  13524  tanhlt1  13563  sin01bnd  13588  cos01bnd  13589  eirrlem  13605  bitsmod  13751  mulgcd  13849  prmind2  13893  mulgcddvds  13909  qnumgt0  13947  iserodd  14021  pcpremul  14029  fldivp1  14078  pcfaclem  14079  qexpz  14082  prmpwdvds  14084  pockthg  14086  prmreclem1  14096  prmreclem5  14100  4sqlem10  14127  4sqlem12  14136  4sqlem16  14140  4sqlem17  14141  vdwlem3  14163  vdwlem8  14168  vdwlem9  14169  0ram  14200  ramz2  14204  xpsc0  14618  xpsc1  14619  odmulg  16179  dfod2  16187  odf1o1  16193  odf1o2  16194  sylow3lem4  16251  ablsub4  16424  odadd1  16452  odadd2  16453  ablfacrp2  16691  ablfac1b  16694  ablfac1eu  16697  pgpfac1lem3a  16700  pgpfaclem2  16706  chrcong  18086  znrrg  18124  cygznlem1  18125  txdis  19338  txdis1cn  19341  ptunhmeo  19514  divstgplem  19824  blcld  20213  nlmvscnlem2  20399  blcvx  20508  metds0  20559  metdseq0  20563  icopnfcnv  20647  lebnumii  20671  ipcau2  20882  tchcphlem1  20883  ipcnlem2  20889  csbren  21031  trirn  21032  dyadf  21205  dyadovol  21207  dyaddisjlem  21209  dyadmaxlem  21211  opnmbllem  21215  mbfmulc2lem  21259  mbfi1fseqlem4  21330  mbfi1fseqlem5  21331  mbfi1fseqlem6  21332  itg2mulclem  21358  itg2monolem1  21362  itg2monolem3  21364  itg2cnlem2  21374  itgabs  21446  dvlip  21599  dvlt0  21611  dvcvx  21626  ftc1lem4  21645  dgrcolem2  21875  aaliou3lem2  21943  aaliou3lem9  21950  itgulm  22007  radcnvlem1  22012  abelthlem2  22031  abelthlem7  22037  tangtx  22101  cosne0  22120  cosordlem  22121  tanord1  22127  logdivlti  22203  logcnlem4  22224  logf1o2  22229  cxpcn3lem  22319  cxpaddle  22324  ang180lem2  22340  atanlogsublem  22444  atantan  22452  atanbndlem  22454  atans2  22460  leibpi  22471  log2tlbnd  22474  birthdaylem3  22481  efrlim  22497  jensenlem2  22515  ftalem1  22544  ftalem5  22548  basellem1  22552  basellem4  22555  fsumdvdsdiaglem  22657  dvdsflf1o  22661  fsumfldivdiaglem  22663  ppiub  22677  mersenne  22700  dchrptlem1  22737  bposlem1  22757  bposlem2  22758  bposlem4  22760  lgsdilem  22795  lgseisenlem1  22822  lgseisenlem2  22823  lgseisenlem3  22824  lgsquadlem1  22827  lgsquadlem2  22828  2sqlem3  22839  2sqlem8  22845  2sqlem11  22848  2sqblem  22850  chebbnd1lem2  22853  chebbnd1lem3  22854  rplogsumlem1  22867  rplogsumlem2  22868  dchrisumlem1  22872  dchrmusum2  22877  dchrisum0flblem1  22891  mulog2sumlem1  22917  logdivbnd  22939  pntpbnd1a  22968  pntpbnd1  22969  pntpbnd2  22970  pntlemh  22982  pntlemr  22985  pntlemk  22989  pntlemo  22990  ostth2lem1  23001  ostth2lem2  23017  ostth2lem3  23018  ostth3  23021  tglineineq  23188  tglineinteq  23190  axsegcon  23326  axpaschlem  23339  vdgrun  23724  vdgrfiun  23725  eupath2lem3  23753  gxmodid  23919  nmbdoplbi  25581  nmcoplbi  25585  nmophmi  25588  nmbdfnlbi  25606  nmcfnlbi  25609  cnlnadjlem7  25630  nmopcoi  25652  resf1o  26182  xdivrec  26248  unitdivcld  26477  measvunilem  26772  measvuni  26774  measssd  26775  measiuns  26777  measinblem  26780  measdivcst  26785  oddpwdc  26882  probun  26947  totprobd  26954  dstrvprob  26999  zetacvg  27146  subfaclim  27221  conpcon  27269  cvmliftlem2  27320  cvmliftlem6  27324  cvmliftlem7  27325  cvmliftlem8  27326  cvmliftlem9  27327  cvmliftlem10  27328  snmlff  27363  lineext  28252  hilbert1.1  28330  opnmbllem0  28576  ismblfin  28581  itgabsnc  28610  ftc1cnnclem  28614  nn0prpwlem  28666  bfplem1  28870  bfp  28872  eldioph2lem1  29247  fphpdo  29305  irrapxlem1  29312  irrapxlem2  29313  irrapxlem3  29314  irrapxlem5  29316  pellexlem2  29320  pell1234qrreccl  29344  pell1234qrmulcl  29345  pell1234qrdich  29351  pell1qr1  29361  pellqrexplicit  29367  pellfundex  29376  reglogltb  29381  reglogleb  29382  pellfund14  29388  rmspecsqrnq  29396  rmxycomplete  29407  jm2.24nn  29451  jm2.17b  29453  jm2.17c  29454  jm2.18  29486  jm2.19lem2  29488  jm2.20nn  29495  jm2.16nn0  29502  jm3.1lem2  29516  areaquad  29741  stoweidlem1  29945  stoweidlem11  29955  stoweidlem14  29958  stoweidlem26  29970  stoweidlem34  29978  stoweidlem38  29982  stoweidlem60  30004  clwwlkf1  30607  domnmsuppn0  30931  lincvalpr  31085  ldepspr  31140  islindeps2  31150  cpdmatlem3  31327  lfl1  33054  lfladdcl  33055  eqlkr  33083  lkrlsp  33086  atcvrj2b  33415  3dim1  33450  3dim2  33451  llni2  33495  2llnjaN  33549  lvoli3  33560  lvoli2  33564  lncvrelatN  33764  lhpat4N  34027  lhpat3  34029  4atexlemex6  34057  ldilco  34099  ltrnid  34118  ltrnatb  34120  ltrnel  34122  ltrncnvel  34125  ltrncnv  34129  ltrn11at  34130  ltrneq  34132  ltrnmw  34134  trlat  34152  trlator0  34154  ltrnnidn  34157  trlid0  34159  trlnidatb  34160  trlnle  34169  trlval3  34170  trlval4  34171  cdlemc2  34175  cdlemc5  34178  cdlemc6  34179  cdlemc  34180  cdlemd2  34182  cdlemd9  34189  cdleme0e  34200  cdleme02N  34205  cdleme0ex1N  34206  cdleme3e  34215  cdleme3g  34217  cdleme3h  34218  cdleme3  34220  cdleme7aa  34225  cdleme7b  34227  cdleme7c  34228  cdleme7d  34229  cdleme7e  34230  cdleme7ga  34231  cdleme7  34232  cdleme9  34236  cdleme16aN  34242  cdleme11c  34244  cdleme11dN  34245  cdleme11e  34246  cdleme11h  34249  cdleme11j  34250  cdleme11k  34251  cdleme12  34254  cdleme21j  34319  cdleme26eALTN  34344  cdleme26f  34346  cdleme26f2  34348  cdlemefrs29bpre0  34379  cdleme35a  34431  cdleme35b  34433  cdleme35c  34434  cdleme35f  34437  cdleme36a  34443  cdleme38m  34446  cdlemeg46rgv  34511  cdlemeg46req  34512  cdlemf  34546  cdlemg2fvlem  34577  cdlemg2l  34586  cdlemg7N  34609  cdlemg12g  34632  cdlemg15  34639  cdlemg17h  34651  cdlemg17  34660  cdlemg19a  34666  cdlemg24  34671  cdlemg37  34672  cdlemg27a  34675  cdlemg31b0N  34677  cdlemg27b  34679  cdlemg31c  34682  cdlemg31d  34683  cdlemg35  34696  trljco  34723  tgrpgrplem  34732  cdlemh2  34799  tendoconid  34812  tendotr  34813  cdlemk35s-id  34921  cdlemk39s-id  34923  cdlemk53b  34939  cdlemk53  34940  cdlemk54  34941  cdleml3N  34961  cdleml5N  34963  tendospcanN  35007  diclss  35177  dihvalcq2  35231  dihord4  35242  dihord5b  35243  dihord5apre  35246  dihmeetlem1N  35274  dihmeetbclemN  35288  dihmeetlem20N  35310  dihmeetALTN  35311  dihatlat  35318  dihatexv  35322  dochkr1  35462  dochkr1OLDN  35463  lcfl7lem  35483  lclkrlem2m  35503  hdmaplna1  35894  hdmaplns1  35895  hdmaplnm1  35896
  Copyright terms: Public domain W3C validator