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

Theorem syl112anc 1188
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 519 . 2  |-  ( ph  ->  ( th  /\  ta ) )
6 syl112anc.5 . 2  |-  ( ( ps  /\  ch  /\  ( th  /\  ta )
)  ->  et )
71, 2, 5, 6syl3anc 1184 1  |-  ( ph  ->  et )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  fveqf1o  5988  gruina  8649  grur1  8651  enqeq  8767  recrec  9667  rec11r  9669  divdivdiv  9671  dmdcan  9680  ddcan  9684  rereccl  9688  div2neg  9693  divmuld  9768  divmul2d  9779  divmul3d  9780  divassd  9781  div12d  9782  div23d  9783  divdird  9784  divsubdird  9785  div11d  9786  ltmul12a  9822  ltdiv1  9830  ltrec  9847  lt2msq1  9849  lediv2  9856  supmul1  9929  qbtwnre  10741  xlemul1a  10823  xlemul1  10825  xadd4d  10838  quoremz  11191  quoremnn0ALT  11193  expgt1  11373  nnlesq  11439  expnbnd  11463  expmulnbnd  11466  discr1  11470  facubnd  11546  hashf1lem1  11659  sqrlem6  12008  mulcn2  12344  climcnds  12586  geomulcvg  12608  cvgrat  12615  eftlub  12665  eflegeo  12677  tanhlt1  12716  sin01bnd  12741  cos01bnd  12742  eirrlem  12758  bitsmod  12903  mulgcd  13001  prmind2  13045  mulgcddvds  13059  qnumgt0  13097  iserodd  13164  pcpremul  13172  fldivp1  13221  pcfaclem  13222  qexpz  13225  prmpwdvds  13227  pockthg  13229  prmreclem1  13239  prmreclem5  13243  4sqlem10  13270  4sqlem12  13279  4sqlem16  13283  4sqlem17  13284  vdwlem3  13306  vdwlem8  13311  vdwlem9  13312  0ram  13343  ramz2  13347  xpsc0  13740  xpsc1  13741  odmulg  15147  dfod2  15155  odf1o1  15161  odf1o2  15162  sylow3lem4  15219  ablsub4  15392  odadd1  15418  odadd2  15419  ablfacrp2  15580  ablfac1b  15583  ablfac1eu  15586  pgpfac1lem3a  15589  pgpfaclem2  15595  chrcong  16765  znrrg  16801  cygznlem1  16802  txdis  17617  txdis1cn  17620  ptunhmeo  17793  divstgplem  18103  blcld  18488  nlmvscnlem2  18674  blcvx  18782  metds0  18833  metdseq0  18837  icopnfcnv  18920  lebnumii  18944  ipcau2  19144  tchcphlem1  19145  ipcnlem2  19151  dyadf  19436  dyadovol  19438  dyaddisjlem  19440  dyadmaxlem  19442  opnmbllem  19446  mbfmulc2lem  19492  mbfi1fseqlem4  19563  mbfi1fseqlem5  19564  mbfi1fseqlem6  19565  itg2mulclem  19591  itg2monolem1  19595  itg2monolem3  19597  itg2cnlem2  19607  itgabs  19679  dvlip  19830  dvlt0  19842  dvcvx  19857  ftc1lem4  19876  dgrcolem2  20145  aaliou3lem2  20213  aaliou3lem9  20220  itgulm  20277  radcnvlem1  20282  abelthlem2  20301  abelthlem7  20307  tangtx  20366  cosne0  20385  cosordlem  20386  tanord1  20392  logdivlti  20468  logcnlem4  20489  logf1o2  20494  cxpcn3lem  20584  cxpaddle  20589  ang180lem2  20605  atanlogsublem  20708  atantan  20716  atanbndlem  20718  atans2  20724  leibpi  20735  log2tlbnd  20738  birthdaylem3  20745  efrlim  20761  jensenlem2  20779  ftalem1  20808  ftalem5  20812  basellem1  20816  basellem4  20819  fsumdvdsdiaglem  20921  dvdsflf1o  20925  fsumfldivdiaglem  20927  ppiub  20941  mersenne  20964  dchrptlem1  21001  bposlem1  21021  bposlem2  21022  bposlem4  21024  lgsdilem  21059  lgseisenlem1  21086  lgseisenlem2  21087  lgseisenlem3  21088  lgsquadlem1  21091  lgsquadlem2  21092  2sqlem3  21103  2sqlem8  21109  2sqlem11  21112  2sqblem  21114  chebbnd1lem2  21117  chebbnd1lem3  21118  rplogsumlem1  21131  rplogsumlem2  21132  dchrisumlem1  21136  dchrmusum2  21141  dchrisum0flblem1  21155  mulog2sumlem1  21181  logdivbnd  21203  pntpbnd1a  21232  pntpbnd1  21233  pntpbnd2  21234  pntlemh  21246  pntlemr  21249  pntlemk  21253  pntlemo  21254  ostth2lem1  21265  ostth2lem2  21281  ostth2lem3  21282  ostth3  21285  vdgrun  21625  vdgrfiun  21626  eupath2lem3  21654  gxmodid  21820  nmbdoplbi  23480  nmcoplbi  23484  nmophmi  23487  nmbdfnlbi  23505  nmcfnlbi  23508  cnlnadjlem7  23529  nmopcoi  23551  xdivrec  24126  unitdivcld  24252  measvunilem  24519  measvuni  24521  measssd  24522  measiuns  24524  measinblem  24527  measdivcst  24532  probun  24630  totprobd  24637  dstrvprob  24682  zetacvg  24752  subfaclim  24827  conpcon  24875  cvmliftlem2  24926  cvmliftlem6  24930  cvmliftlem7  24931  cvmliftlem8  24932  cvmliftlem9  24933  cvmliftlem10  24934  snmlff  24969  axsegcon  25770  axpaschlem  25783  lineext  25914  hilbert1.1  25992  ismblfin  26146  itgabsnc  26173  ftc1cnnclem  26177  nn0prpwlem  26215  csbrn  26346  trirn  26347  bfplem1  26421  bfp  26423  eldioph2lem1  26708  fphpdo  26768  irrapxlem1  26775  irrapxlem2  26776  irrapxlem3  26777  irrapxlem5  26779  pellexlem2  26783  pell1234qrreccl  26807  pell1234qrmulcl  26808  pell1234qrdich  26814  pell1qr1  26824  pellqrexplicit  26830  pellfundex  26839  reglogltb  26844  reglogleb  26845  pellfund14  26851  rmspecsqrnq  26859  rmxycomplete  26870  jm2.24nn  26914  jm2.17b  26916  jm2.17c  26917  jm2.18  26949  jm2.19lem2  26951  jm2.20nn  26958  jm2.16nn0  26965  jm3.1lem2  26979  enfixsn  27125  stoweidlem1  27617  stoweidlem11  27627  stoweidlem14  27630  stoweidlem26  27642  stoweidlem34  27650  stoweidlem38  27654  stoweidlem60  27676  lfl1  29553  lfladdcl  29554  eqlkr  29582  lkrlsp  29585  atcvrj2b  29914  3dim1  29949  3dim2  29950  llni2  29994  2llnjaN  30048  lvoli3  30059  lvoli2  30063  lncvrelatN  30263  lhpat4N  30526  lhpat3  30528  4atexlemex6  30556  ldilco  30598  ltrnid  30617  ltrnatb  30619  ltrnel  30621  ltrncnvel  30624  ltrncnv  30628  ltrn11at  30629  ltrneq  30631  ltrnmw  30633  trlat  30651  trlator0  30653  ltrnnidn  30656  trlid0  30658  trlnidatb  30659  trlnle  30668  trlval3  30669  trlval4  30670  cdlemc2  30674  cdlemc5  30677  cdlemc6  30678  cdlemc  30679  cdlemd2  30681  cdlemd9  30688  cdleme0e  30699  cdleme02N  30704  cdleme0ex1N  30705  cdleme3e  30714  cdleme3g  30716  cdleme3h  30717  cdleme3  30719  cdleme7aa  30724  cdleme7b  30726  cdleme7c  30727  cdleme7d  30728  cdleme7e  30729  cdleme7ga  30730  cdleme7  30731  cdleme9  30735  cdleme16aN  30741  cdleme11c  30743  cdleme11dN  30744  cdleme11e  30745  cdleme11h  30748  cdleme11j  30749  cdleme11k  30750  cdleme12  30753  cdleme21j  30818  cdleme26eALTN  30843  cdleme26f  30845  cdleme26f2  30847  cdlemefrs29bpre0  30878  cdleme35a  30930  cdleme35b  30932  cdleme35c  30933  cdleme35f  30936  cdleme36a  30942  cdleme38m  30945  cdlemeg46rgv  31010  cdlemeg46req  31011  cdlemf  31045  cdlemg2fvlem  31076  cdlemg2l  31085  cdlemg7N  31108  cdlemg12g  31131  cdlemg15  31138  cdlemg17h  31150  cdlemg17  31159  cdlemg19a  31165  cdlemg24  31170  cdlemg37  31171  cdlemg27a  31174  cdlemg31b0N  31176  cdlemg27b  31178  cdlemg31c  31181  cdlemg31d  31182  cdlemg35  31195  trljco  31222  tgrpgrplem  31231  cdlemh2  31298  tendoconid  31311  tendotr  31312  cdlemk35s-id  31420  cdlemk39s-id  31422  cdlemk53b  31438  cdlemk53  31439  cdlemk54  31440  cdleml3N  31460  cdleml5N  31462  tendospcanN  31506  diclss  31676  dihvalcq2  31730  dihord4  31741  dihord5b  31742  dihord5apre  31745  dihmeetlem1N  31773  dihmeetbclemN  31787  dihmeetlem20N  31809  dihmeetALTN  31810  dihatlat  31817  dihatexv  31821  dochkr1  31961  dochkr1OLDN  31962  lcfl7lem  31982  lclkrlem2m  32002  hdmaplna1  32393  hdmaplns1  32394  hdmaplnm1  32395
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator