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

Theorem syl112anc 1232
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 1228 1  |-  ( ph  ->  et )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973
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 975
This theorem is referenced by:  rmob2  3433  fveqf1o  6191  enfixsn  7623  gruina  9192  grur1  9194  enqeq  9308  recrec  10237  rec11r  10239  divdivdiv  10241  dmdcan  10250  ddcan  10254  rereccl  10258  div2neg  10263  divmuld  10338  divmul2d  10349  divmul3d  10350  divassd  10351  div12d  10352  div23d  10353  divdird  10354  divsubdird  10355  div11d  10356  ltmul12a  10394  ltdiv1  10402  ltrec  10422  lt2msq1  10424  lediv2  10431  supmul1  10504  qbtwnre  11394  xlemul1a  11476  xlemul1  11478  xadd4d  11491  quoremz  11946  quoremnn0ALT  11948  expgt1  12168  nnlesq  12235  expnbnd  12259  expmulnbnd  12262  discr1  12266  facubnd  12342  hashf1lem1  12466  2swrdeqwrdeq  12637  sqrlem6  13040  mulcn2  13377  climcnds  13622  geomulcvg  13644  cvgrat  13651  eftlub  13701  eflegeo  13713  tanhlt1  13752  sin01bnd  13777  cos01bnd  13778  eirrlem  13794  bitsmod  13941  mulgcd  14039  prmind2  14083  mulgcddvds  14100  qnumgt0  14138  iserodd  14214  pcpremul  14222  fldivp1  14271  pcfaclem  14272  qexpz  14275  prmpwdvds  14277  pockthg  14279  prmreclem1  14289  prmreclem5  14293  4sqlem10  14320  4sqlem12  14329  4sqlem16  14333  4sqlem17  14334  vdwlem3  14356  vdwlem8  14361  vdwlem9  14362  0ram  14393  ramz2  14397  xpsc0  14811  xpsc1  14812  odmulg  16374  dfod2  16382  odf1o1  16388  odf1o2  16389  sylow3lem4  16446  ablsub4  16619  odadd1  16647  odadd2  16648  ablfacrp2  16908  ablfac1b  16911  ablfac1eu  16914  pgpfac1lem3a  16917  pgpfaclem2  16923  chrcong  18333  znrrg  18371  cygznlem1  18372  chpdmatlem3  19108  txdis  19868  txdis1cn  19871  ptunhmeo  20044  divstgplem  20354  blcld  20743  nlmvscnlem2  20929  blcvx  21038  metds0  21089  metdseq0  21093  icopnfcnv  21177  lebnumii  21201  ipcau2  21412  tchcphlem1  21413  ipcnlem2  21419  csbren  21561  trirn  21562  dyadf  21735  dyadovol  21737  dyaddisjlem  21739  dyadmaxlem  21741  opnmbllem  21745  mbfmulc2lem  21789  mbfi1fseqlem4  21860  mbfi1fseqlem5  21861  mbfi1fseqlem6  21862  itg2mulclem  21888  itg2monolem1  21892  itg2monolem3  21894  itg2cnlem2  21904  itgabs  21976  dvlip  22129  dvlt0  22141  dvcvx  22156  ftc1lem4  22175  dgrcolem2  22405  aaliou3lem2  22473  aaliou3lem9  22480  itgulm  22537  radcnvlem1  22542  abelthlem2  22561  abelthlem7  22567  tangtx  22631  cosne0  22650  cosordlem  22651  tanord1  22657  logdivlti  22733  logcnlem4  22754  logf1o2  22759  cxpcn3lem  22849  cxpaddle  22854  ang180lem2  22870  atanlogsublem  22974  atantan  22982  atanbndlem  22984  atans2  22990  leibpi  23001  log2tlbnd  23004  birthdaylem3  23011  efrlim  23027  jensenlem2  23045  ftalem1  23074  ftalem5  23078  basellem1  23082  basellem4  23085  fsumdvdsdiaglem  23187  dvdsflf1o  23191  fsumfldivdiaglem  23193  ppiub  23207  mersenne  23230  dchrptlem1  23267  bposlem1  23287  bposlem2  23288  bposlem4  23290  lgsdilem  23325  lgseisenlem1  23352  lgseisenlem2  23353  lgseisenlem3  23354  lgsquadlem1  23357  lgsquadlem2  23358  2sqlem3  23369  2sqlem8  23375  2sqlem11  23378  2sqblem  23380  chebbnd1lem2  23383  chebbnd1lem3  23384  rplogsumlem1  23397  rplogsumlem2  23398  dchrisumlem1  23402  dchrmusum2  23407  dchrisum0flblem1  23421  mulog2sumlem1  23447  logdivbnd  23469  pntpbnd1a  23498  pntpbnd1  23499  pntpbnd2  23500  pntlemh  23512  pntlemr  23515  pntlemk  23519  pntlemo  23520  ostth2lem1  23531  ostth2lem2  23547  ostth2lem3  23548  ostth3  23551  tglineineq  23736  tglineinteq  23738  axsegcon  23906  axpaschlem  23919  clwwlkf1  24472  vdgrun  24577  vdgrfiun  24578  eupath2lem3  24655  gxmodid  24957  nmbdoplbi  26619  nmcoplbi  26623  nmophmi  26626  nmbdfnlbi  26644  nmcfnlbi  26647  cnlnadjlem7  26668  nmopcoi  26690  resf1o  27225  xdivrec  27291  txomap  27500  unitdivcld  27519  measvunilem  27823  measvuni  27825  measssd  27826  measiuns  27828  measinblem  27831  measdivcst  27836  oddpwdc  27933  probun  27998  totprobd  28005  dstrvprob  28050  zetacvg  28197  subfaclim  28272  conpcon  28320  cvmliftlem2  28371  cvmliftlem6  28375  cvmliftlem7  28376  cvmliftlem8  28377  cvmliftlem9  28378  cvmliftlem10  28379  snmlff  28414  lineext  29303  hilbert1.1  29381  opnmbllem0  29627  ismblfin  29632  itgabsnc  29661  ftc1cnnclem  29665  nn0prpwlem  29717  bfplem1  29921  bfp  29923  eldioph2lem1  30297  fphpdo  30355  irrapxlem1  30362  irrapxlem2  30363  irrapxlem3  30364  irrapxlem5  30366  pellexlem2  30370  pell1234qrreccl  30394  pell1234qrmulcl  30395  pell1234qrdich  30401  pell1qr1  30411  pellqrexplicit  30417  pellfundex  30426  reglogltb  30431  reglogleb  30432  pellfund14  30438  rmspecsqrtnq  30446  rmxycomplete  30457  jm2.24nn  30501  jm2.17b  30503  jm2.17c  30504  jm2.18  30534  jm2.19lem2  30536  jm2.20nn  30543  jm2.16nn0  30550  jm3.1lem2  30564  areaquad  30789  stoweidlem1  31301  stoweidlem11  31311  stoweidlem14  31314  stoweidlem26  31326  stoweidlem34  31334  stoweidlem38  31338  stoweidlem60  31360  domnmsuppn0  32035  lincvalpr  32092  ldepspr  32147  islindeps2  32157  lfl1  33867  lfladdcl  33868  eqlkr  33896  lkrlsp  33899  atcvrj2b  34228  3dim1  34263  3dim2  34264  llni2  34308  2llnjaN  34362  lvoli3  34373  lvoli2  34377  lncvrelatN  34577  lhpat4N  34840  lhpat3  34842  4atexlemex6  34870  ldilco  34912  ltrnid  34931  ltrnatb  34933  ltrnel  34935  ltrncnvel  34938  ltrncnv  34942  ltrn11at  34943  ltrneq  34945  ltrnmw  34947  trlat  34965  trlator0  34967  ltrnnidn  34970  trlid0  34972  trlnidatb  34973  trlnle  34982  trlval3  34983  trlval4  34984  cdlemc2  34988  cdlemc5  34991  cdlemc6  34992  cdlemc  34993  cdlemd2  34995  cdlemd9  35002  cdleme0e  35013  cdleme02N  35018  cdleme0ex1N  35019  cdleme3e  35028  cdleme3g  35030  cdleme3h  35031  cdleme3  35033  cdleme7aa  35038  cdleme7b  35040  cdleme7c  35041  cdleme7d  35042  cdleme7e  35043  cdleme7ga  35044  cdleme7  35045  cdleme9  35049  cdleme16aN  35055  cdleme11c  35057  cdleme11dN  35058  cdleme11e  35059  cdleme11h  35062  cdleme11j  35063  cdleme11k  35064  cdleme12  35067  cdleme21j  35132  cdleme26eALTN  35157  cdleme26f  35159  cdleme26f2  35161  cdlemefrs29bpre0  35192  cdleme35a  35244  cdleme35b  35246  cdleme35c  35247  cdleme35f  35250  cdleme36a  35256  cdleme38m  35259  cdlemeg46rgv  35324  cdlemeg46req  35325  cdlemf  35359  cdlemg2fvlem  35390  cdlemg2l  35399  cdlemg7N  35422  cdlemg12g  35445  cdlemg15  35452  cdlemg17h  35464  cdlemg17  35473  cdlemg19a  35479  cdlemg24  35484  cdlemg37  35485  cdlemg27a  35488  cdlemg31b0N  35490  cdlemg27b  35492  cdlemg31c  35495  cdlemg31d  35496  cdlemg35  35509  trljco  35536  tgrpgrplem  35545  cdlemh2  35612  tendoconid  35625  tendotr  35626  cdlemk35s-id  35734  cdlemk39s-id  35736  cdlemk53b  35752  cdlemk53  35753  cdlemk54  35754  cdleml3N  35774  cdleml5N  35776  tendospcanN  35820  diclss  35990  dihvalcq2  36044  dihord4  36055  dihord5b  36056  dihord5apre  36059  dihmeetlem1N  36087  dihmeetbclemN  36101  dihmeetlem20N  36123  dihmeetALTN  36124  dihatlat  36131  dihatexv  36135  dochkr1  36275  dochkr1OLDN  36276  lcfl7lem  36296  lclkrlem2m  36316  hdmaplna1  36707  hdmaplns1  36708  hdmaplnm1  36709
  Copyright terms: Public domain W3C validator