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

Theorem syl112anc 1268
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 534 . 2  |-  ( ph  ->  ( th  /\  ta ) )
6 syl112anc.5 . 2  |-  ( ( ps  /\  ch  /\  ( th  /\  ta )
)  ->  et )
71, 2, 5, 6syl3anc 1264 1  |-  ( ph  ->  et )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  rmob2  3329  fveqf1o  6152  enfixsn  7627  gruina  9187  grur1  9189  enqeq  9303  recrec  10248  rec11r  10250  divdivdiv  10252  dmdcan  10261  ddcan  10265  rereccl  10269  div2neg  10274  divmuld  10349  divmul2d  10360  divmul3d  10361  divassd  10362  div12d  10363  div23d  10364  divdird  10365  divsubdird  10366  div11d  10367  ltmul12a  10405  ltdiv1  10413  ltrec  10432  lt2msq1  10434  lediv2  10440  supmul1  10520  qbtwnre  11436  xlemul1a  11518  xlemul1  11520  xadd4d  11533  quoremz  12025  quoremnn0ALT  12027  expgt1  12253  nnlesq  12321  expnbnd  12344  expmulnbnd  12347  discr1  12351  facubnd  12428  hashf1lem1  12559  2swrdeqwrdeq  12748  sqrlem6  13248  mulcn2  13595  climcnds  13845  geomulcvg  13868  cvgrat  13875  eftlub  14099  eflegeo  14111  tanhlt1  14150  sin01bnd  14175  cos01bnd  14176  eirrlem  14192  bitsmod  14346  mulgcd  14450  prmind2  14571  mulgcddvds  14597  qnumgt0  14635  iserodd  14721  pcpremul  14729  fldivp1  14778  pcfaclem  14779  qexpz  14782  prmpwdvds  14784  pockthg  14786  prmreclem1  14796  prmreclem5  14800  4sqlem10  14827  4sqlem12  14836  4sqlem16OLD  14840  4sqlem17OLD  14841  4sqlem16  14846  4sqlem17  14847  vdwlem3  14869  vdwlem8  14874  vdwlem9  14875  0ram  14914  ramz2  14918  xpsc0  15402  xpsc1  15403  odmulg  17143  dfod2  17151  odf1o1  17157  odf1o2  17158  sylow3lem4  17218  ablsub4  17391  odadd1  17422  odadd2  17423  ablfacrp2  17636  ablfac1b  17639  ablfac1eu  17642  pgpfac1lem3a  17645  pgpfaclem2  17651  chrcong  19035  znrrg  19071  cygznlem1  19072  chpdmatlem3  19799  txdis  20582  txdis1cn  20585  ptunhmeo  20758  qustgplem  21070  blcld  21455  nlmvscnlem2  21623  blcvx  21751  metds0  21802  metdseq0  21806  metds0OLD  21817  metdseq0OLD  21821  icopnfcnv  21905  lebnumii  21932  ipcau2  22143  tchcphlem1  22144  ipcnlem2  22150  csbren  22288  trirn  22289  dyadf  22484  dyadovol  22486  dyaddisjlem  22488  dyadmaxlem  22490  opnmbllem  22494  mbfmulc2lem  22538  mbfi1fseqlem4  22611  mbfi1fseqlem5  22612  mbfi1fseqlem6  22613  itg2mulclem  22639  itg2monolem1  22643  itg2monolem3  22645  itg2cnlem2  22655  itgabs  22727  dvlip  22880  dvlt0  22892  dvcvx  22907  ftc1lem4  22926  dgrcolem2  23163  aaliou3lem2  23234  aaliou3lem9  23241  itgulm  23298  radcnvlem1  23303  abelthlem2  23322  abelthlem7  23328  tangtx  23395  cosne0  23414  cosordlem  23415  tanord1  23421  logdivlti  23504  logcnlem4  23525  logf1o2  23530  cxpcn3lem  23622  cxpaddle  23627  ang180lem2  23674  atanlogsublem  23776  atantan  23784  atanbndlem  23786  atans2  23792  leibpi  23803  log2tlbnd  23806  birthdaylem3  23814  efrlim  23830  jensenlem2  23848  zetacvg  23875  ftalem1  23932  ftalem5  23936  ftalem5OLD  23938  basellem1  23942  basellem4  23945  fsumdvdsdiaglem  24047  dvdsflf1o  24051  fsumfldivdiaglem  24053  ppiub  24067  mersenne  24090  dchrptlem1  24127  bposlem1  24147  bposlem2  24148  bposlem4  24150  lgsdilem  24185  lgseisenlem1  24212  lgseisenlem2  24213  lgseisenlem3  24214  lgsquadlem1  24217  lgsquadlem2  24218  2sqlem3  24229  2sqlem8  24235  2sqlem11  24238  2sqblem  24240  chebbnd1lem2  24243  chebbnd1lem3  24244  rplogsumlem1  24257  rplogsumlem2  24258  dchrisumlem1  24262  dchrmusum2  24267  dchrisum0flblem1  24281  mulog2sumlem1  24307  logdivbnd  24329  pntpbnd1a  24358  pntpbnd1  24359  pntpbnd2  24360  pntlemh  24372  pntlemr  24375  pntlemk  24379  pntlemo  24380  ostth2lem1  24391  ostth2lem2  24407  ostth2lem3  24408  ostth3  24411  legov  24565  axsegcon  24892  axpaschlem  24905  clwwlkf1  25459  vdgrun  25564  vdgrfiun  25565  eupath2lem3  25642  gxmodid  25942  nmbdoplbi  27612  nmcoplbi  27616  nmophmi  27619  nmbdfnlbi  27637  nmcfnlbi  27640  cnlnadjlem7  27661  nmopcoi  27683  resf1o  28258  xdivrec  28340  txomap  28606  unitdivcld  28652  measvunilem  28979  measvuni  28981  measssd  28982  measiuns  28984  measinblem  28987  measdivcst  28992  sibfof  29118  oddpwdc  29132  sseqfv1  29167  sseqfv2  29172  probun  29197  totprobd  29204  dstrvprob  29249  subfaclim  29856  conpcon  29903  cvmliftlem2  29954  cvmliftlem6  29958  cvmliftlem7  29959  cvmliftlem8  29960  cvmliftlem9  29961  cvmliftlem10  29962  snmlff  29997  lineext  30785  hilbert1.1  30863  nn0prpwlem  30920  poimirlem1  31842  opnmbllem0  31877  ismblfin  31882  itgabsnc  31912  ftc1cnnclem  31916  bfplem1  32055  bfp  32057  lfl1  32542  lfladdcl  32543  eqlkr  32571  lkrlsp  32574  atcvrj2b  32903  3dim1  32938  3dim2  32939  llni2  32983  2llnjaN  33037  lvoli3  33048  lvoli2  33052  lncvrelatN  33252  lhpat4N  33515  lhpat3  33517  4atexlemex6  33545  ldilco  33587  ltrnid  33606  ltrnatb  33608  ltrnel  33610  ltrncnvel  33613  ltrncnv  33617  ltrn11at  33618  ltrneq  33620  ltrnmwOLD  33623  trlat  33641  trlator0  33643  ltrnnidn  33646  trlid0  33648  trlnidatb  33649  trlnle  33658  trlval3  33659  trlval4  33660  cdlemc2  33664  cdlemc5  33667  cdlemc6  33668  cdlemc  33669  cdlemd2  33671  cdlemd9  33678  cdleme0e  33689  cdleme02N  33694  cdleme0ex1N  33695  cdleme3e  33704  cdleme3g  33706  cdleme3h  33707  cdleme3  33709  cdleme7aa  33714  cdleme7b  33716  cdleme7c  33717  cdleme7d  33718  cdleme7e  33719  cdleme7ga  33720  cdleme7  33721  cdleme9  33725  cdleme16aN  33731  cdleme11c  33733  cdleme11dN  33734  cdleme11e  33735  cdleme11h  33738  cdleme11j  33739  cdleme11k  33740  cdleme12  33743  cdleme21j  33809  cdleme26eALTN  33834  cdleme26f  33836  cdleme26f2  33838  cdlemefrs29bpre0  33869  cdleme35a  33921  cdleme35b  33923  cdleme35c  33924  cdleme35f  33927  cdleme36a  33933  cdleme38m  33936  cdlemeg46rgv  34001  cdlemeg46req  34002  cdlemf  34036  cdlemg2fvlem  34067  cdlemg2l  34076  cdlemg7N  34099  cdlemg12g  34122  cdlemg15  34129  cdlemg17h  34141  cdlemg17  34150  cdlemg19a  34156  cdlemg24  34161  cdlemg37  34162  cdlemg27a  34165  cdlemg31b0N  34167  cdlemg27b  34169  cdlemg31c  34172  cdlemg31d  34173  cdlemg35  34186  trljco  34213  tgrpgrplem  34222  cdlemh2  34289  tendoconid  34302  tendotr  34303  cdlemk35s-id  34411  cdlemk39s-id  34413  cdlemk53b  34429  cdlemk53  34430  cdlemk54  34431  cdleml3N  34451  cdleml5N  34453  tendospcanN  34497  diclss  34667  dihvalcq2  34721  dihord4  34732  dihord5b  34733  dihord5apre  34736  dihmeetlem1N  34764  dihmeetbclemN  34778  dihmeetlem20N  34800  dihmeetALTN  34801  dihatlat  34808  dihatexv  34812  dochkr1  34952  dochkr1OLDN  34953  lcfl7lem  34973  lclkrlem2m  34993  hdmaplna1  35384  hdmaplns1  35385  hdmaplnm1  35386  eldioph2lem1  35508  fphpdo  35566  irrapxlem1  35573  irrapxlem2  35574  irrapxlem3  35575  irrapxlem5  35577  pellexlem2  35581  pell1234qrreccl  35607  pell1234qrmulcl  35608  pell1234qrdich  35614  pell1qr1  35624  pellqrexplicit  35630  pellfundex  35641  reglogltb  35646  reglogleb  35647  pellfund14  35653  rmspecsqrtnq  35661  rmxycomplete  35672  jm2.24nn  35716  jm2.17b  35718  jm2.17c  35719  jm2.18  35750  jm2.19lem2  35752  jm2.20nn  35759  jm2.16nn0  35766  jm3.1lem2  35780  areaquad  36008  lemuldiv3d  36522  lemuldiv4d  36523  stoweidlem1  37738  stoweidlem11  37748  stoweidlem14  37751  stoweidlem26  37763  stoweidlem34  37772  stoweidlem38  37776  stoweidlem60  37798  fourierdlem52  37899  etransclem38  38014  pfxsuffeqwrdeq  38754  domnmsuppn0  39741  lincvalpr  39798  ldepspr  39853  islindeps2  39863  fldivexpfllog2  39963
  Copyright terms: Public domain W3C validator