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  3399  fveqf1o  6215  enfixsn  7687  gruina  9242  grur1  9244  enqeq  9358  recrec  10303  rec11r  10305  divdivdiv  10307  dmdcan  10316  ddcan  10320  rereccl  10324  div2neg  10329  divmuld  10404  divmul2d  10415  divmul3d  10416  divassd  10417  div12d  10418  div23d  10419  divdird  10420  divsubdird  10421  div11d  10422  ltmul12a  10460  ltdiv1  10468  ltrec  10487  lt2msq1  10489  lediv2  10496  supmul1  10576  qbtwnre  11492  xlemul1a  11574  xlemul1  11576  xadd4d  11589  quoremz  12079  quoremnn0ALT  12081  expgt1  12307  nnlesq  12375  expnbnd  12398  expmulnbnd  12401  discr1  12405  facubnd  12482  hashf1lem1  12613  2swrdeqwrdeq  12794  sqrlem6  13290  mulcn2  13637  climcnds  13887  geomulcvg  13910  cvgrat  13917  eftlub  14141  eflegeo  14153  tanhlt1  14192  sin01bnd  14217  cos01bnd  14218  eirrlem  14234  bitsmod  14384  mulgcd  14485  prmind2  14606  mulgcddvds  14632  qnumgt0  14670  iserodd  14748  pcpremul  14756  fldivp1  14805  pcfaclem  14806  qexpz  14809  prmpwdvds  14811  pockthg  14813  prmreclem1  14823  prmreclem5  14827  4sqlem10  14854  4sqlem12  14863  4sqlem16OLD  14867  4sqlem17OLD  14868  4sqlem16  14873  4sqlem17  14874  vdwlem3  14896  vdwlem8  14901  vdwlem9  14902  0ram  14941  ramz2  14945  xpsc0  15417  xpsc1  15418  odmulg  17145  dfod2  17153  odf1o1  17159  odf1o2  17160  sylow3lem4  17217  ablsub4  17390  odadd1  17421  odadd2  17422  ablfacrp2  17635  ablfac1b  17638  ablfac1eu  17641  pgpfac1lem3a  17644  pgpfaclem2  17650  chrcong  19031  znrrg  19067  cygznlem1  19068  chpdmatlem3  19795  txdis  20578  txdis1cn  20581  ptunhmeo  20754  qustgplem  21066  blcld  21451  nlmvscnlem2  21619  blcvx  21727  metds0  21778  metdseq0  21782  icopnfcnv  21866  lebnumii  21890  ipcau2  22101  tchcphlem1  22102  ipcnlem2  22108  csbren  22246  trirn  22247  dyadf  22426  dyadovol  22428  dyaddisjlem  22430  dyadmaxlem  22432  opnmbllem  22436  mbfmulc2lem  22480  mbfi1fseqlem4  22553  mbfi1fseqlem5  22554  mbfi1fseqlem6  22555  itg2mulclem  22581  itg2monolem1  22585  itg2monolem3  22587  itg2cnlem2  22597  itgabs  22669  dvlip  22822  dvlt0  22834  dvcvx  22849  ftc1lem4  22868  dgrcolem2  23096  aaliou3lem2  23164  aaliou3lem9  23171  itgulm  23228  radcnvlem1  23233  abelthlem2  23252  abelthlem7  23258  tangtx  23325  cosne0  23344  cosordlem  23345  tanord1  23351  logdivlti  23434  logcnlem4  23455  logf1o2  23460  cxpcn3lem  23552  cxpaddle  23557  ang180lem2  23604  atanlogsublem  23706  atantan  23714  atanbndlem  23716  atans2  23722  leibpi  23733  log2tlbnd  23736  birthdaylem3  23744  efrlim  23760  jensenlem2  23778  zetacvg  23805  ftalem1  23862  ftalem5  23866  basellem1  23870  basellem4  23873  fsumdvdsdiaglem  23975  dvdsflf1o  23979  fsumfldivdiaglem  23981  ppiub  23995  mersenne  24018  dchrptlem1  24055  bposlem1  24075  bposlem2  24076  bposlem4  24078  lgsdilem  24113  lgseisenlem1  24140  lgseisenlem2  24141  lgseisenlem3  24142  lgsquadlem1  24145  lgsquadlem2  24146  2sqlem3  24157  2sqlem8  24163  2sqlem11  24166  2sqblem  24168  chebbnd1lem2  24171  chebbnd1lem3  24172  rplogsumlem1  24185  rplogsumlem2  24186  dchrisumlem1  24190  dchrmusum2  24195  dchrisum0flblem1  24209  mulog2sumlem1  24235  logdivbnd  24257  pntpbnd1a  24286  pntpbnd1  24287  pntpbnd2  24288  pntlemh  24300  pntlemr  24303  pntlemk  24307  pntlemo  24308  ostth2lem1  24319  ostth2lem2  24335  ostth2lem3  24336  ostth3  24339  legov  24490  axsegcon  24803  axpaschlem  24816  clwwlkf1  25369  vdgrun  25474  vdgrfiun  25475  eupath2lem3  25552  gxmodid  25852  nmbdoplbi  27512  nmcoplbi  27516  nmophmi  27519  nmbdfnlbi  27537  nmcfnlbi  27540  cnlnadjlem7  27561  nmopcoi  27583  resf1o  28158  xdivrec  28234  txomap  28500  unitdivcld  28546  measvunilem  28873  measvuni  28875  measssd  28876  measiuns  28878  measinblem  28881  measdivcst  28886  sibfof  29001  oddpwdc  29013  sseqfv1  29048  sseqfv2  29053  probun  29078  totprobd  29085  dstrvprob  29130  subfaclim  29699  conpcon  29746  cvmliftlem2  29797  cvmliftlem6  29801  cvmliftlem7  29802  cvmliftlem8  29803  cvmliftlem9  29804  cvmliftlem10  29805  snmlff  29840  lineext  30628  hilbert1.1  30706  nn0prpwlem  30763  poimirlem1  31645  opnmbllem0  31680  ismblfin  31685  itgabsnc  31715  ftc1cnnclem  31719  bfplem1  31858  bfp  31860  lfl1  32345  lfladdcl  32346  eqlkr  32374  lkrlsp  32377  atcvrj2b  32706  3dim1  32741  3dim2  32742  llni2  32786  2llnjaN  32840  lvoli3  32851  lvoli2  32855  lncvrelatN  33055  lhpat4N  33318  lhpat3  33320  4atexlemex6  33348  ldilco  33390  ltrnid  33409  ltrnatb  33411  ltrnel  33413  ltrncnvel  33416  ltrncnv  33420  ltrn11at  33421  ltrneq  33423  ltrnmwOLD  33426  trlat  33444  trlator0  33446  ltrnnidn  33449  trlid0  33451  trlnidatb  33452  trlnle  33461  trlval3  33462  trlval4  33463  cdlemc2  33467  cdlemc5  33470  cdlemc6  33471  cdlemc  33472  cdlemd2  33474  cdlemd9  33481  cdleme0e  33492  cdleme02N  33497  cdleme0ex1N  33498  cdleme3e  33507  cdleme3g  33509  cdleme3h  33510  cdleme3  33512  cdleme7aa  33517  cdleme7b  33519  cdleme7c  33520  cdleme7d  33521  cdleme7e  33522  cdleme7ga  33523  cdleme7  33524  cdleme9  33528  cdleme16aN  33534  cdleme11c  33536  cdleme11dN  33537  cdleme11e  33538  cdleme11h  33541  cdleme11j  33542  cdleme11k  33543  cdleme12  33546  cdleme21j  33612  cdleme26eALTN  33637  cdleme26f  33639  cdleme26f2  33641  cdlemefrs29bpre0  33672  cdleme35a  33724  cdleme35b  33726  cdleme35c  33727  cdleme35f  33730  cdleme36a  33736  cdleme38m  33739  cdlemeg46rgv  33804  cdlemeg46req  33805  cdlemf  33839  cdlemg2fvlem  33870  cdlemg2l  33879  cdlemg7N  33902  cdlemg12g  33925  cdlemg15  33932  cdlemg17h  33944  cdlemg17  33953  cdlemg19a  33959  cdlemg24  33964  cdlemg37  33965  cdlemg27a  33968  cdlemg31b0N  33970  cdlemg27b  33972  cdlemg31c  33975  cdlemg31d  33976  cdlemg35  33989  trljco  34016  tgrpgrplem  34025  cdlemh2  34092  tendoconid  34105  tendotr  34106  cdlemk35s-id  34214  cdlemk39s-id  34216  cdlemk53b  34232  cdlemk53  34233  cdlemk54  34234  cdleml3N  34254  cdleml5N  34256  tendospcanN  34300  diclss  34470  dihvalcq2  34524  dihord4  34535  dihord5b  34536  dihord5apre  34539  dihmeetlem1N  34567  dihmeetbclemN  34581  dihmeetlem20N  34603  dihmeetALTN  34604  dihatlat  34611  dihatexv  34615  dochkr1  34755  dochkr1OLDN  34756  lcfl7lem  34776  lclkrlem2m  34796  hdmaplna1  35187  hdmaplns1  35188  hdmaplnm1  35189  eldioph2lem1  35311  fphpdo  35369  irrapxlem1  35376  irrapxlem2  35377  irrapxlem3  35378  irrapxlem5  35380  pellexlem2  35384  pell1234qrreccl  35408  pell1234qrmulcl  35409  pell1234qrdich  35415  pell1qr1  35425  pellqrexplicit  35431  pellfundex  35440  reglogltb  35445  reglogleb  35446  pellfund14  35452  rmspecsqrtnq  35460  rmxycomplete  35471  jm2.24nn  35515  jm2.17b  35517  jm2.17c  35518  jm2.18  35549  jm2.19lem2  35551  jm2.20nn  35558  jm2.16nn0  35565  jm3.1lem2  35579  areaquad  35800  lemuldiv3d  36252  lemuldiv4d  36253  stoweidlem1  37430  stoweidlem11  37440  stoweidlem14  37443  stoweidlem26  37455  stoweidlem34  37464  stoweidlem38  37468  stoweidlem60  37490  fourierdlem52  37590  etransclem38  37704  pfxsuffeqwrdeq  38337  domnmsuppn0  38914  lincvalpr  38971  ldepspr  39026  islindeps2  39036  fldivexpfllog2  39137
  Copyright terms: Public domain W3C validator