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

Theorem syl112anc 1280
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 539 . 2  |-  ( ph  ->  ( th  /\  ta ) )
6 syl112anc.5 . 2  |-  ( ( ps  /\  ch  /\  ( th  /\  ta )
)  ->  et )
71, 2, 5, 6syl3anc 1276 1  |-  ( ph  ->  et )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375    /\ w3a 991
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 190  df-an 377  df-3an 993
This theorem is referenced by:  rmob2  3372  fveqf1o  6224  enfixsn  7706  gruina  9268  grur1  9270  enqeq  9384  recrec  10331  rec11r  10333  divdivdiv  10335  dmdcan  10344  ddcan  10348  rereccl  10352  div2neg  10357  divmuld  10432  divmul2d  10443  divmul3d  10444  divassd  10445  div12d  10446  div23d  10447  divdird  10448  divsubdird  10449  div11d  10450  ltmul12a  10488  ltdiv1  10496  ltrec  10515  lt2msq1  10517  lediv2  10523  supmul1  10603  qbtwnre  11520  xlemul1a  11602  xlemul1  11604  xadd4d  11617  quoremz  12113  quoremnn0ALT  12115  expgt1  12341  nnlesq  12409  expnbnd  12432  expmulnbnd  12435  discr1  12439  facubnd  12516  hashf1lem1  12650  2swrdeqwrdeq  12845  sqrlem6  13359  mulcn2  13707  climcnds  13957  geomulcvg  13980  cvgrat  13987  eftlub  14211  eflegeo  14223  tanhlt1  14262  sin01bnd  14287  cos01bnd  14288  eirrlem  14304  bitsmod  14458  mulgcd  14562  prmind2  14683  mulgcddvds  14709  qnumgt0  14747  iserodd  14833  pcpremul  14841  fldivp1  14890  pcfaclem  14891  qexpz  14894  prmpwdvds  14896  pockthg  14898  prmreclem1  14908  prmreclem5  14912  4sqlem10  14939  4sqlem12  14948  4sqlem16OLD  14952  4sqlem17OLD  14953  4sqlem16  14958  4sqlem17  14959  vdwlem3  14981  vdwlem8  14986  vdwlem9  14987  0ram  15026  ramz2  15030  xpsc0  15514  xpsc1  15515  odmulg  17255  dfod2  17263  odf1o1  17269  odf1o2  17270  sylow3lem4  17330  ablsub4  17503  odadd1  17534  odadd2  17535  ablfacrp2  17748  ablfac1b  17751  ablfac1eu  17754  pgpfac1lem3a  17757  pgpfaclem2  17763  chrcong  19148  znrrg  19184  cygznlem1  19185  chpdmatlem3  19912  txdis  20695  txdis1cn  20698  ptunhmeo  20871  qustgplem  21183  blcld  21568  nlmvscnlem2  21736  blcvx  21864  metds0  21915  metdseq0  21919  metds0OLD  21930  metdseq0OLD  21934  icopnfcnv  22018  lebnumii  22045  ipcau2  22256  tchcphlem1  22257  ipcnlem2  22263  csbren  22401  trirn  22402  dyadf  22597  dyadovol  22599  dyaddisjlem  22601  dyadmaxlem  22603  opnmbllem  22607  mbfmulc2lem  22651  mbfi1fseqlem4  22724  mbfi1fseqlem5  22725  mbfi1fseqlem6  22726  itg2mulclem  22752  itg2monolem1  22756  itg2monolem3  22758  itg2cnlem2  22768  itgabs  22840  dvlip  22993  dvlt0  23005  dvcvx  23020  ftc1lem4  23039  dgrcolem2  23276  aaliou3lem2  23347  aaliou3lem9  23354  itgulm  23411  radcnvlem1  23416  abelthlem2  23435  abelthlem7  23441  tangtx  23508  cosne0  23527  cosordlem  23528  tanord1  23534  logdivlti  23617  logcnlem4  23638  logf1o2  23643  cxpcn3lem  23735  cxpaddle  23740  ang180lem2  23787  atanlogsublem  23889  atantan  23897  atanbndlem  23899  atans2  23905  leibpi  23916  log2tlbnd  23919  birthdaylem3  23927  efrlim  23943  jensenlem2  23961  zetacvg  23988  ftalem1  24045  ftalem5  24049  ftalem5OLD  24051  basellem1  24055  basellem4  24058  fsumdvdsdiaglem  24160  dvdsflf1o  24164  fsumfldivdiaglem  24166  ppiub  24180  mersenne  24203  dchrptlem1  24240  bposlem1  24260  bposlem2  24261  bposlem4  24263  lgsdilem  24298  lgseisenlem1  24325  lgseisenlem2  24326  lgseisenlem3  24327  lgsquadlem1  24330  lgsquadlem2  24331  2sqlem3  24342  2sqlem8  24348  2sqlem11  24351  2sqblem  24353  chebbnd1lem2  24356  chebbnd1lem3  24357  rplogsumlem1  24370  rplogsumlem2  24371  dchrisumlem1  24375  dchrmusum2  24380  dchrisum0flblem1  24394  mulog2sumlem1  24420  logdivbnd  24442  pntpbnd1a  24471  pntpbnd1  24472  pntpbnd2  24473  pntlemh  24485  pntlemr  24488  pntlemk  24492  pntlemo  24493  ostth2lem1  24504  ostth2lem2  24520  ostth2lem3  24521  ostth3  24524  legov  24678  axsegcon  25005  axpaschlem  25018  clwwlkf1  25572  vdgrun  25677  vdgrfiun  25678  eupath2lem3  25755  gxmodid  26055  nmbdoplbi  27725  nmcoplbi  27729  nmophmi  27732  nmbdfnlbi  27750  nmcfnlbi  27753  cnlnadjlem7  27774  nmopcoi  27796  resf1o  28363  xdivrec  28444  txomap  28709  unitdivcld  28755  measvunilem  29082  measvuni  29084  measssd  29085  measiuns  29087  measinblem  29090  measdivcst  29095  sibfof  29221  oddpwdc  29235  sseqfv1  29270  sseqfv2  29275  probun  29300  totprobd  29307  dstrvprob  29352  subfaclim  29959  conpcon  30006  cvmliftlem2  30057  cvmliftlem6  30061  cvmliftlem7  30062  cvmliftlem8  30063  cvmliftlem9  30064  cvmliftlem10  30065  snmlff  30100  lineext  30891  hilbert1.1  30969  nn0prpwlem  31026  poimirlem1  31985  opnmbllem0  32020  ismblfin  32025  itgabsnc  32055  ftc1cnnclem  32059  bfplem1  32198  bfp  32200  lfl1  32680  lfladdcl  32681  eqlkr  32709  lkrlsp  32712  atcvrj2b  33041  3dim1  33076  3dim2  33077  llni2  33121  2llnjaN  33175  lvoli3  33186  lvoli2  33190  lncvrelatN  33390  lhpat4N  33653  lhpat3  33655  4atexlemex6  33683  ldilco  33725  ltrnid  33744  ltrnatb  33746  ltrnel  33748  ltrncnvel  33751  ltrncnv  33755  ltrn11at  33756  ltrneq  33758  ltrnmwOLD  33761  trlat  33779  trlator0  33781  ltrnnidn  33784  trlid0  33786  trlnidatb  33787  trlnle  33796  trlval3  33797  trlval4  33798  cdlemc2  33802  cdlemc5  33805  cdlemc6  33806  cdlemc  33807  cdlemd2  33809  cdlemd9  33816  cdleme0e  33827  cdleme02N  33832  cdleme0ex1N  33833  cdleme3e  33842  cdleme3g  33844  cdleme3h  33845  cdleme3  33847  cdleme7aa  33852  cdleme7b  33854  cdleme7c  33855  cdleme7d  33856  cdleme7e  33857  cdleme7ga  33858  cdleme7  33859  cdleme9  33863  cdleme16aN  33869  cdleme11c  33871  cdleme11dN  33872  cdleme11e  33873  cdleme11h  33876  cdleme11j  33877  cdleme11k  33878  cdleme12  33881  cdleme21j  33947  cdleme26eALTN  33972  cdleme26f  33974  cdleme26f2  33976  cdlemefrs29bpre0  34007  cdleme35a  34059  cdleme35b  34061  cdleme35c  34062  cdleme35f  34065  cdleme36a  34071  cdleme38m  34074  cdlemeg46rgv  34139  cdlemeg46req  34140  cdlemf  34174  cdlemg2fvlem  34205  cdlemg2l  34214  cdlemg7N  34237  cdlemg12g  34260  cdlemg15  34267  cdlemg17h  34279  cdlemg17  34288  cdlemg19a  34294  cdlemg24  34299  cdlemg37  34300  cdlemg27a  34303  cdlemg31b0N  34305  cdlemg27b  34307  cdlemg31c  34310  cdlemg31d  34311  cdlemg35  34324  trljco  34351  tgrpgrplem  34360  cdlemh2  34427  tendoconid  34440  tendotr  34441  cdlemk35s-id  34549  cdlemk39s-id  34551  cdlemk53b  34567  cdlemk53  34568  cdlemk54  34569  cdleml3N  34589  cdleml5N  34591  tendospcanN  34635  diclss  34805  dihvalcq2  34859  dihord4  34870  dihord5b  34871  dihord5apre  34874  dihmeetlem1N  34902  dihmeetbclemN  34916  dihmeetlem20N  34938  dihmeetALTN  34939  dihatlat  34946  dihatexv  34950  dochkr1  35090  dochkr1OLDN  35091  lcfl7lem  35111  lclkrlem2m  35131  hdmaplna1  35522  hdmaplns1  35523  hdmaplnm1  35524  eldioph2lem1  35646  fphpdo  35704  irrapxlem1  35710  irrapxlem2  35711  irrapxlem3  35712  irrapxlem5  35714  pellexlem2  35718  pell1234qrreccl  35744  pell1234qrmulcl  35745  pell1234qrdich  35751  pell1qr1  35761  pellqrexplicit  35767  pellfundex  35778  reglogltb  35783  reglogleb  35784  pellfund14  35790  rmspecsqrtnq  35798  rmxycomplete  35809  jm2.24nn  35853  jm2.17b  35855  jm2.17c  35856  jm2.18  35887  jm2.19lem2  35889  jm2.20nn  35896  jm2.16nn0  35903  jm3.1lem2  35917  areaquad  36145  lemuldiv3d  36659  lemuldiv4d  36660  stoweidlem1  37898  stoweidlem11  37908  stoweidlem14  37911  stoweidlem26  37923  stoweidlem34  37932  stoweidlem38  37936  stoweidlem60  37958  fourierdlem52  38059  etransclem38  38174  pfxsuffeqwrdeq  38986  0uhgrsubgr  39400  upgr4cycl4dv4e  39925  domnmsuppn0  40426  lincvalpr  40483  ldepspr  40538  islindeps2  40548  fldivexpfllog2  40648
  Copyright terms: Public domain W3C validator