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

Theorem syl112anc 1230
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 530 . 2  |-  ( ph  ->  ( th  /\  ta ) )
6 syl112anc.5 . 2  |-  ( ( ps  /\  ch  /\  ( th  /\  ta )
)  ->  et )
71, 2, 5, 6syl3anc 1226 1  |-  ( ph  ->  et )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 971
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 369  df-3an 973
This theorem is referenced by:  rmob2  3418  fveqf1o  6180  enfixsn  7619  gruina  9185  grur1  9187  enqeq  9301  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  10421  lt2msq1  10423  lediv2  10430  supmul1  10503  qbtwnre  11401  xlemul1a  11483  xlemul1  11485  xadd4d  11498  quoremz  11964  quoremnn0ALT  11966  expgt1  12189  nnlesq  12256  expnbnd  12280  expmulnbnd  12283  discr1  12287  facubnd  12363  hashf1lem1  12491  2swrdeqwrdeq  12672  sqrlem6  13166  mulcn2  13503  climcnds  13748  geomulcvg  13770  cvgrat  13777  eftlub  13929  eflegeo  13941  tanhlt1  13980  sin01bnd  14005  cos01bnd  14006  eirrlem  14022  bitsmod  14173  mulgcd  14271  prmind2  14315  mulgcddvds  14332  qnumgt0  14370  iserodd  14446  pcpremul  14454  fldivp1  14503  pcfaclem  14504  qexpz  14507  prmpwdvds  14509  pockthg  14511  prmreclem1  14521  prmreclem5  14525  4sqlem10  14552  4sqlem12  14561  4sqlem16  14565  4sqlem17  14566  vdwlem3  14588  vdwlem8  14593  vdwlem9  14594  0ram  14625  ramz2  14629  xpsc0  15052  xpsc1  15053  odmulg  16780  dfod2  16788  odf1o1  16794  odf1o2  16795  sylow3lem4  16852  ablsub4  17025  odadd1  17056  odadd2  17057  ablfacrp2  17316  ablfac1b  17319  ablfac1eu  17322  pgpfac1lem3a  17325  pgpfaclem2  17331  chrcong  18744  znrrg  18780  cygznlem1  18781  chpdmatlem3  19511  txdis  20302  txdis1cn  20305  ptunhmeo  20478  qustgplem  20788  blcld  21177  nlmvscnlem2  21363  blcvx  21472  metds0  21523  metdseq0  21527  icopnfcnv  21611  lebnumii  21635  ipcau2  21846  tchcphlem1  21847  ipcnlem2  21853  csbren  21995  trirn  21996  dyadf  22169  dyadovol  22171  dyaddisjlem  22173  dyadmaxlem  22175  opnmbllem  22179  mbfmulc2lem  22223  mbfi1fseqlem4  22294  mbfi1fseqlem5  22295  mbfi1fseqlem6  22296  itg2mulclem  22322  itg2monolem1  22326  itg2monolem3  22328  itg2cnlem2  22338  itgabs  22410  dvlip  22563  dvlt0  22575  dvcvx  22590  ftc1lem4  22609  dgrcolem2  22840  aaliou3lem2  22908  aaliou3lem9  22915  itgulm  22972  radcnvlem1  22977  abelthlem2  22996  abelthlem7  23002  tangtx  23067  cosne0  23086  cosordlem  23087  tanord1  23093  logdivlti  23176  logcnlem4  23197  logf1o2  23202  cxpcn3lem  23292  cxpaddle  23297  ang180lem2  23344  atanlogsublem  23446  atantan  23454  atanbndlem  23456  atans2  23462  leibpi  23473  log2tlbnd  23476  birthdaylem3  23484  efrlim  23500  jensenlem2  23518  ftalem1  23547  ftalem5  23551  basellem1  23555  basellem4  23558  fsumdvdsdiaglem  23660  dvdsflf1o  23664  fsumfldivdiaglem  23666  ppiub  23680  mersenne  23703  dchrptlem1  23740  bposlem1  23760  bposlem2  23761  bposlem4  23763  lgsdilem  23798  lgseisenlem1  23825  lgseisenlem2  23826  lgseisenlem3  23827  lgsquadlem1  23830  lgsquadlem2  23831  2sqlem3  23842  2sqlem8  23848  2sqlem11  23851  2sqblem  23853  chebbnd1lem2  23856  chebbnd1lem3  23857  rplogsumlem1  23870  rplogsumlem2  23871  dchrisumlem1  23875  dchrmusum2  23880  dchrisum0flblem1  23894  mulog2sumlem1  23920  logdivbnd  23942  pntpbnd1a  23971  pntpbnd1  23972  pntpbnd2  23973  pntlemh  23985  pntlemr  23988  pntlemk  23992  pntlemo  23993  ostth2lem1  24004  ostth2lem2  24020  ostth2lem3  24021  ostth3  24024  legov  24176  axsegcon  24435  axpaschlem  24448  clwwlkf1  25001  vdgrun  25106  vdgrfiun  25107  eupath2lem3  25184  gxmodid  25482  nmbdoplbi  27144  nmcoplbi  27148  nmophmi  27151  nmbdfnlbi  27169  nmcfnlbi  27172  cnlnadjlem7  27193  nmopcoi  27215  resf1o  27787  xdivrec  27860  txomap  28075  unitdivcld  28121  measvunilem  28423  measvuni  28425  measssd  28426  measiuns  28428  measinblem  28431  measdivcst  28436  sibfof  28549  oddpwdc  28560  sseqfv1  28595  sseqfv2  28600  probun  28625  totprobd  28632  dstrvprob  28677  zetacvg  28824  subfaclim  28899  conpcon  28947  cvmliftlem2  28998  cvmliftlem6  29002  cvmliftlem7  29003  cvmliftlem8  29004  cvmliftlem9  29005  cvmliftlem10  29006  snmlff  29041  lineext  29957  hilbert1.1  30035  opnmbllem0  30293  ismblfin  30298  itgabsnc  30327  ftc1cnnclem  30331  nn0prpwlem  30383  bfplem1  30561  bfp  30563  eldioph2lem1  30935  fphpdo  30993  irrapxlem1  31000  irrapxlem2  31001  irrapxlem3  31002  irrapxlem5  31004  pellexlem2  31008  pell1234qrreccl  31032  pell1234qrmulcl  31033  pell1234qrdich  31039  pell1qr1  31049  pellqrexplicit  31055  pellfundex  31064  reglogltb  31069  reglogleb  31070  pellfund14  31076  rmspecsqrtnq  31084  rmxycomplete  31095  jm2.24nn  31139  jm2.17b  31141  jm2.17c  31142  jm2.18  31172  jm2.19lem2  31174  jm2.20nn  31181  jm2.16nn0  31188  jm3.1lem2  31202  areaquad  31428  stoweidlem1  32025  stoweidlem11  32035  stoweidlem14  32038  stoweidlem26  32050  stoweidlem34  32058  stoweidlem38  32062  stoweidlem60  32084  fourierdlem52  32183  etransclem38  32297  pfxsuffeqwrdeq  32653  domnmsuppn0  33235  lincvalpr  33292  ldepspr  33347  islindeps2  33357  fldivexpfllog2  33459  lfl1  35211  lfladdcl  35212  eqlkr  35240  lkrlsp  35243  atcvrj2b  35572  3dim1  35607  3dim2  35608  llni2  35652  2llnjaN  35706  lvoli3  35717  lvoli2  35721  lncvrelatN  35921  lhpat4N  36184  lhpat3  36186  4atexlemex6  36214  ldilco  36256  ltrnid  36275  ltrnatb  36277  ltrnel  36279  ltrncnvel  36282  ltrncnv  36286  ltrn11at  36287  ltrneq  36289  ltrnmwOLD  36292  trlat  36310  trlator0  36312  ltrnnidn  36315  trlid0  36317  trlnidatb  36318  trlnle  36327  trlval3  36328  trlval4  36329  cdlemc2  36333  cdlemc5  36336  cdlemc6  36337  cdlemc  36338  cdlemd2  36340  cdlemd9  36347  cdleme0e  36358  cdleme02N  36363  cdleme0ex1N  36364  cdleme3e  36373  cdleme3g  36375  cdleme3h  36376  cdleme3  36378  cdleme7aa  36383  cdleme7b  36385  cdleme7c  36386  cdleme7d  36387  cdleme7e  36388  cdleme7ga  36389  cdleme7  36390  cdleme9  36394  cdleme16aN  36400  cdleme11c  36402  cdleme11dN  36403  cdleme11e  36404  cdleme11h  36407  cdleme11j  36408  cdleme11k  36409  cdleme12  36412  cdleme21j  36478  cdleme26eALTN  36503  cdleme26f  36505  cdleme26f2  36507  cdlemefrs29bpre0  36538  cdleme35a  36590  cdleme35b  36592  cdleme35c  36593  cdleme35f  36596  cdleme36a  36602  cdleme38m  36605  cdlemeg46rgv  36670  cdlemeg46req  36671  cdlemf  36705  cdlemg2fvlem  36736  cdlemg2l  36745  cdlemg7N  36768  cdlemg12g  36791  cdlemg15  36798  cdlemg17h  36810  cdlemg17  36819  cdlemg19a  36825  cdlemg24  36830  cdlemg37  36831  cdlemg27a  36834  cdlemg31b0N  36836  cdlemg27b  36838  cdlemg31c  36841  cdlemg31d  36842  cdlemg35  36855  trljco  36882  tgrpgrplem  36891  cdlemh2  36958  tendoconid  36971  tendotr  36972  cdlemk35s-id  37080  cdlemk39s-id  37082  cdlemk53b  37098  cdlemk53  37099  cdlemk54  37100  cdleml3N  37120  cdleml5N  37122  tendospcanN  37166  diclss  37336  dihvalcq2  37390  dihord4  37401  dihord5b  37402  dihord5apre  37405  dihmeetlem1N  37433  dihmeetbclemN  37447  dihmeetlem20N  37469  dihmeetALTN  37470  dihatlat  37477  dihatexv  37481  dochkr1  37621  dochkr1OLDN  37622  lcfl7lem  37642  lclkrlem2m  37662  hdmaplna1  38053  hdmaplns1  38054  hdmaplnm1  38055  lemuldiv3d  38520  lemuldiv4d  38521
  Copyright terms: Public domain W3C validator