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

Theorem syl112anc 1189
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 520 . 2  |-  ( ph  ->  ( th  /\  ta ) )
6 syl112anc.5 . 2  |-  ( ( ps  /\  ch  /\  ( th  /\  ta )
)  ->  et )
71, 2, 5, 6syl3anc 1185 1  |-  ( ph  ->  et )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  fveqf1o  6058  gruina  8724  grur1  8726  enqeq  8842  recrec  9742  rec11r  9744  divdivdiv  9746  dmdcan  9755  ddcan  9759  rereccl  9763  div2neg  9768  divmuld  9843  divmul2d  9854  divmul3d  9855  divassd  9856  div12d  9857  div23d  9858  divdird  9859  divsubdird  9860  div11d  9861  ltmul12a  9897  ltdiv1  9905  ltrec  9922  lt2msq1  9924  lediv2  9931  supmul1  10004  qbtwnre  10816  xlemul1a  10898  xlemul1  10900  xadd4d  10913  quoremz  11267  quoremnn0ALT  11269  expgt1  11449  nnlesq  11515  expnbnd  11539  expmulnbnd  11542  discr1  11546  facubnd  11622  hashf1lem1  11735  sqrlem6  12084  mulcn2  12420  climcnds  12662  geomulcvg  12684  cvgrat  12691  eftlub  12741  eflegeo  12753  tanhlt1  12792  sin01bnd  12817  cos01bnd  12818  eirrlem  12834  bitsmod  12979  mulgcd  13077  prmind2  13121  mulgcddvds  13135  qnumgt0  13173  iserodd  13240  pcpremul  13248  fldivp1  13297  pcfaclem  13298  qexpz  13301  prmpwdvds  13303  pockthg  13305  prmreclem1  13315  prmreclem5  13319  4sqlem10  13346  4sqlem12  13355  4sqlem16  13359  4sqlem17  13360  vdwlem3  13382  vdwlem8  13387  vdwlem9  13388  0ram  13419  ramz2  13423  xpsc0  13816  xpsc1  13817  odmulg  15223  dfod2  15231  odf1o1  15237  odf1o2  15238  sylow3lem4  15295  ablsub4  15468  odadd1  15494  odadd2  15495  ablfacrp2  15656  ablfac1b  15659  ablfac1eu  15662  pgpfac1lem3a  15665  pgpfaclem2  15671  chrcong  16841  znrrg  16877  cygznlem1  16878  txdis  17695  txdis1cn  17698  ptunhmeo  17871  divstgplem  18181  blcld  18566  nlmvscnlem2  18752  blcvx  18860  metds0  18911  metdseq0  18915  icopnfcnv  18998  lebnumii  19022  ipcau2  19222  tchcphlem1  19223  ipcnlem2  19229  dyadf  19514  dyadovol  19516  dyaddisjlem  19518  dyadmaxlem  19520  opnmbllem  19524  mbfmulc2lem  19568  mbfi1fseqlem4  19639  mbfi1fseqlem5  19640  mbfi1fseqlem6  19641  itg2mulclem  19667  itg2monolem1  19671  itg2monolem3  19673  itg2cnlem2  19683  itgabs  19755  dvlip  19908  dvlt0  19920  dvcvx  19935  ftc1lem4  19954  dgrcolem2  20223  aaliou3lem2  20291  aaliou3lem9  20298  itgulm  20355  radcnvlem1  20360  abelthlem2  20379  abelthlem7  20385  tangtx  20444  cosne0  20463  cosordlem  20464  tanord1  20470  logdivlti  20546  logcnlem4  20567  logf1o2  20572  cxpcn3lem  20662  cxpaddle  20667  ang180lem2  20683  atanlogsublem  20786  atantan  20794  atanbndlem  20796  atans2  20802  leibpi  20813  log2tlbnd  20816  birthdaylem3  20823  efrlim  20839  jensenlem2  20857  ftalem1  20886  ftalem5  20890  basellem1  20894  basellem4  20897  fsumdvdsdiaglem  20999  dvdsflf1o  21003  fsumfldivdiaglem  21005  ppiub  21019  mersenne  21042  dchrptlem1  21079  bposlem1  21099  bposlem2  21100  bposlem4  21102  lgsdilem  21137  lgseisenlem1  21164  lgseisenlem2  21165  lgseisenlem3  21166  lgsquadlem1  21169  lgsquadlem2  21170  2sqlem3  21181  2sqlem8  21187  2sqlem11  21190  2sqblem  21192  chebbnd1lem2  21195  chebbnd1lem3  21196  rplogsumlem1  21209  rplogsumlem2  21210  dchrisumlem1  21214  dchrmusum2  21219  dchrisum0flblem1  21233  mulog2sumlem1  21259  logdivbnd  21281  pntpbnd1a  21310  pntpbnd1  21311  pntpbnd2  21312  pntlemh  21324  pntlemr  21327  pntlemk  21331  pntlemo  21332  ostth2lem1  21343  ostth2lem2  21359  ostth2lem3  21360  ostth3  21363  vdgrun  21703  vdgrfiun  21704  eupath2lem3  21732  gxmodid  21898  nmbdoplbi  23558  nmcoplbi  23562  nmophmi  23565  nmbdfnlbi  23583  nmcfnlbi  23586  cnlnadjlem7  23607  nmopcoi  23629  xdivrec  24204  unitdivcld  24330  measvunilem  24597  measvuni  24599  measssd  24600  measiuns  24602  measinblem  24605  measdivcst  24610  probun  24708  totprobd  24715  dstrvprob  24760  zetacvg  24830  subfaclim  24905  conpcon  24953  cvmliftlem2  25004  cvmliftlem6  25008  cvmliftlem7  25009  cvmliftlem8  25010  cvmliftlem9  25011  cvmliftlem10  25012  snmlff  25047  axsegcon  25897  axpaschlem  25910  lineext  26041  hilbert1.1  26119  opnmbllem0  26278  ismblfin  26283  itgabsnc  26312  ftc1cnnclem  26316  nn0prpwlem  26363  csbrn  26494  trirn  26495  bfplem1  26569  bfp  26571  eldioph2lem1  26856  fphpdo  26916  irrapxlem1  26923  irrapxlem2  26924  irrapxlem3  26925  irrapxlem5  26927  pellexlem2  26931  pell1234qrreccl  26955  pell1234qrmulcl  26956  pell1234qrdich  26962  pell1qr1  26972  pellqrexplicit  26978  pellfundex  26987  reglogltb  26992  reglogleb  26993  pellfund14  26999  rmspecsqrnq  27007  rmxycomplete  27018  jm2.24nn  27062  jm2.17b  27064  jm2.17c  27065  jm2.18  27097  jm2.19lem2  27099  jm2.20nn  27106  jm2.16nn0  27113  jm3.1lem2  27127  enfixsn  27272  stoweidlem1  27764  stoweidlem11  27774  stoweidlem14  27777  stoweidlem26  27789  stoweidlem34  27797  stoweidlem38  27801  stoweidlem60  27823  lfl1  29966  lfladdcl  29967  eqlkr  29995  lkrlsp  29998  atcvrj2b  30327  3dim1  30362  3dim2  30363  llni2  30407  2llnjaN  30461  lvoli3  30472  lvoli2  30476  lncvrelatN  30676  lhpat4N  30939  lhpat3  30941  4atexlemex6  30969  ldilco  31011  ltrnid  31030  ltrnatb  31032  ltrnel  31034  ltrncnvel  31037  ltrncnv  31041  ltrn11at  31042  ltrneq  31044  ltrnmw  31046  trlat  31064  trlator0  31066  ltrnnidn  31069  trlid0  31071  trlnidatb  31072  trlnle  31081  trlval3  31082  trlval4  31083  cdlemc2  31087  cdlemc5  31090  cdlemc6  31091  cdlemc  31092  cdlemd2  31094  cdlemd9  31101  cdleme0e  31112  cdleme02N  31117  cdleme0ex1N  31118  cdleme3e  31127  cdleme3g  31129  cdleme3h  31130  cdleme3  31132  cdleme7aa  31137  cdleme7b  31139  cdleme7c  31140  cdleme7d  31141  cdleme7e  31142  cdleme7ga  31143  cdleme7  31144  cdleme9  31148  cdleme16aN  31154  cdleme11c  31156  cdleme11dN  31157  cdleme11e  31158  cdleme11h  31161  cdleme11j  31162  cdleme11k  31163  cdleme12  31166  cdleme21j  31231  cdleme26eALTN  31256  cdleme26f  31258  cdleme26f2  31260  cdlemefrs29bpre0  31291  cdleme35a  31343  cdleme35b  31345  cdleme35c  31346  cdleme35f  31349  cdleme36a  31355  cdleme38m  31358  cdlemeg46rgv  31423  cdlemeg46req  31424  cdlemf  31458  cdlemg2fvlem  31489  cdlemg2l  31498  cdlemg7N  31521  cdlemg12g  31544  cdlemg15  31551  cdlemg17h  31563  cdlemg17  31572  cdlemg19a  31578  cdlemg24  31583  cdlemg37  31584  cdlemg27a  31587  cdlemg31b0N  31589  cdlemg27b  31591  cdlemg31c  31594  cdlemg31d  31595  cdlemg35  31608  trljco  31635  tgrpgrplem  31644  cdlemh2  31711  tendoconid  31724  tendotr  31725  cdlemk35s-id  31833  cdlemk39s-id  31835  cdlemk53b  31851  cdlemk53  31852  cdlemk54  31853  cdleml3N  31873  cdleml5N  31875  tendospcanN  31919  diclss  32089  dihvalcq2  32143  dihord4  32154  dihord5b  32155  dihord5apre  32158  dihmeetlem1N  32186  dihmeetbclemN  32200  dihmeetlem20N  32222  dihmeetALTN  32223  dihatlat  32230  dihatexv  32234  dochkr1  32374  dochkr1OLDN  32375  lcfl7lem  32395  lclkrlem2m  32415  hdmaplna1  32806  hdmaplns1  32807  hdmaplnm1  32808
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator