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

Theorem syl112anc 1186
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 518 . 2  |-  ( ph  ->  ( th  /\  ta ) )
6 syl112anc.5 . 2  |-  ( ( ps  /\  ch  /\  ( th  /\  ta )
)  ->  et )
71, 2, 5, 6syl3anc 1182 1  |-  ( ph  ->  et )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  fveqf1o  5822  gruina  8456  grur1  8458  enqeq  8574  recrec  9473  rec11r  9475  divdivdiv  9477  dmdcan  9486  ddcan  9490  rereccl  9494  div2neg  9499  divmuld  9574  divmul2d  9585  divmul3d  9586  divassd  9587  div12d  9588  div23d  9589  divdird  9590  divsubdird  9591  div11d  9592  ltmul12a  9628  ltdiv1  9636  ltrec  9653  lt2msq1  9655  lediv2  9662  supmul1  9735  qbtwnre  10542  xlemul1a  10624  xlemul1  10626  quoremz  10975  quoremnn0ALT  10977  expgt1  11156  nnlesq  11222  expnbnd  11246  expmulnbnd  11249  discr1  11253  facubnd  11329  hashf1lem1  11409  sqrlem6  11749  mulcn2  12085  climcnds  12326  geomulcvg  12348  cvgrat  12355  eftlub  12405  eflegeo  12417  tanhlt1  12456  sin01bnd  12481  cos01bnd  12482  eirrlem  12498  bitsmod  12643  mulgcd  12741  prmind2  12785  mulgcddvds  12799  qnumgt0  12837  iserodd  12904  pcpremul  12912  fldivp1  12961  pcfaclem  12962  qexpz  12965  prmpwdvds  12967  pockthg  12969  prmreclem1  12979  prmreclem5  12983  4sqlem10  13010  4sqlem12  13019  4sqlem16  13023  4sqlem17  13024  vdwlem3  13046  vdwlem8  13051  vdwlem9  13052  0ram  13083  ramz2  13087  xpsc0  13478  xpsc1  13479  odmulg  14885  dfod2  14893  odf1o1  14899  odf1o2  14900  sylow3lem4  14957  ablsub4  15130  odadd1  15156  odadd2  15157  ablfacrp2  15318  ablfac1b  15321  ablfac1eu  15324  pgpfac1lem3a  15327  pgpfaclem2  15333  chrcong  16499  znrrg  16535  cygznlem1  16536  txdis  17342  txdis1cn  17345  ptunhmeo  17515  divstgplem  17819  blcld  18067  nlmvscnlem2  18212  blcvx  18320  metds0  18370  metdseq0  18374  icopnfcnv  18456  lebnumii  18480  ipcau2  18680  tchcphlem1  18681  ipcnlem2  18687  dyadf  18962  dyadovol  18964  dyaddisjlem  18966  dyadmaxlem  18968  opnmbllem  18972  mbfmulc2lem  19018  mbfi1fseqlem4  19089  mbfi1fseqlem5  19090  mbfi1fseqlem6  19091  itg2mulclem  19117  itg2monolem1  19121  itg2monolem3  19123  itg2cnlem2  19133  itgabs  19205  dvlip  19356  dvlt0  19368  dvcvx  19383  ftc1lem4  19402  dgrcolem2  19671  aaliou3lem2  19739  aaliou3lem9  19746  itgulm  19800  radcnvlem1  19805  abelthlem2  19824  abelthlem7  19830  tangtx  19889  cosne0  19908  cosordlem  19909  tanord1  19915  logdivlti  19987  logcnlem4  20008  logf1o2  20013  cxpcn3lem  20103  cxpaddle  20108  ang180lem2  20124  atanlogsublem  20227  atantan  20235  atanbndlem  20237  atans2  20243  leibpi  20254  log2tlbnd  20257  birthdaylem3  20264  efrlim  20280  jensenlem2  20298  ftalem1  20326  ftalem5  20330  basellem1  20334  basellem4  20337  fsumdvdsdiaglem  20439  dvdsflf1o  20443  fsumfldivdiaglem  20445  ppiub  20459  mersenne  20482  dchrptlem1  20519  bposlem1  20539  bposlem2  20540  bposlem4  20542  lgsdilem  20577  lgseisenlem1  20604  lgseisenlem2  20605  lgseisenlem3  20606  lgsquadlem1  20609  lgsquadlem2  20610  2sqlem3  20621  2sqlem8  20627  2sqlem11  20630  2sqblem  20632  chebbnd1lem2  20635  chebbnd1lem3  20636  rplogsumlem1  20649  rplogsumlem2  20650  dchrisumlem1  20654  dchrmusum2  20659  dchrisum0flblem1  20673  mulog2sumlem1  20699  logdivbnd  20721  pntpbnd1a  20750  pntpbnd1  20751  pntpbnd2  20752  pntlemh  20764  pntlemr  20767  pntlemk  20771  pntlemo  20772  ostth2lem1  20783  ostth2lem2  20799  ostth2lem3  20800  ostth3  20803  gxmodid  20962  nmbdoplbi  22620  nmcoplbi  22624  nmophmi  22627  nmbdfnlbi  22645  nmcfnlbi  22648  cnlnadjlem7  22669  nmopcoi  22691  xdivrec  23126  unitdivcld  23300  esumcst  23451  measvunilem  23555  dya2iocseg  23594  probun  23637  zetacvg  23704  subfaclim  23734  conpcon  23781  cvmliftlem2  23832  cvmliftlem6  23836  cvmliftlem7  23837  cvmliftlem8  23838  cvmliftlem9  23839  cvmliftlem10  23840  vdgrun  23908  eupath2lem3  23918  snmlff  23927  axsegcon  24627  axpaschlem  24640  lineext  24771  hilbert1.1  24849  itgabsnc  25020  ftc1cnnclem  25024  muldisc  25584  limptlimpr2lem1  25677  altretop  25703  cntrset  25705  tcnvec  25793  nn0prpwlem  26341  csbrn  26565  trirn  26566  bfplem1  26649  bfp  26651  eldioph2lem1  26942  fphpdo  27003  irrapxlem1  27010  irrapxlem2  27011  irrapxlem3  27012  irrapxlem5  27014  pellexlem2  27018  pell1234qrreccl  27042  pell1234qrmulcl  27043  pell1234qrdich  27049  pell1qr1  27059  pellqrexplicit  27065  pellfundex  27074  reglogltb  27079  reglogleb  27080  pellfund14  27086  rmspecsqrnq  27094  rmxycomplete  27105  jm2.24nn  27149  jm2.17b  27151  jm2.17c  27152  jm2.18  27184  jm2.19lem2  27186  jm2.20nn  27193  jm2.16nn0  27200  jm3.1lem2  27214  enfixsn  27360  lfl1  29882  lfladdcl  29883  eqlkr  29911  lkrlsp  29914  atcvrj2b  30243  3dim1  30278  3dim2  30279  llni2  30323  2llnjaN  30377  lvoli3  30388  lvoli2  30392  lncvrelatN  30592  lhpat4N  30855  lhpat3  30857  4atexlemex6  30885  ldilco  30927  ltrnid  30946  ltrnatb  30948  ltrnel  30950  ltrncnvel  30953  ltrncnv  30957  ltrn11at  30958  ltrneq  30960  ltrnmw  30962  trlat  30980  trlator0  30982  ltrnnidn  30985  trlid0  30987  trlnidatb  30988  trlnle  30997  trlval3  30998  trlval4  30999  cdlemc2  31003  cdlemc5  31006  cdlemc6  31007  cdlemc  31008  cdlemd2  31010  cdlemd9  31017  cdleme0e  31028  cdleme02N  31033  cdleme0ex1N  31034  cdleme3e  31043  cdleme3g  31045  cdleme3h  31046  cdleme3  31048  cdleme7aa  31053  cdleme7b  31055  cdleme7c  31056  cdleme7d  31057  cdleme7e  31058  cdleme7ga  31059  cdleme7  31060  cdleme9  31064  cdleme16aN  31070  cdleme11c  31072  cdleme11dN  31073  cdleme11e  31074  cdleme11h  31077  cdleme11j  31078  cdleme11k  31079  cdleme12  31082  cdleme21j  31147  cdleme26eALTN  31172  cdleme26f  31174  cdleme26f2  31176  cdlemefrs29bpre0  31207  cdleme35a  31259  cdleme35b  31261  cdleme35c  31262  cdleme35f  31265  cdleme36a  31271  cdleme38m  31274  cdlemeg46rgv  31339  cdlemeg46req  31340  cdlemf  31374  cdlemg2fvlem  31405  cdlemg2l  31414  cdlemg7N  31437  cdlemg12g  31460  cdlemg15  31467  cdlemg17h  31479  cdlemg17  31488  cdlemg19a  31494  cdlemg24  31499  cdlemg37  31500  cdlemg27a  31503  cdlemg31b0N  31505  cdlemg27b  31507  cdlemg31c  31510  cdlemg31d  31511  cdlemg35  31524  trljco  31551  tgrpgrplem  31560  cdlemh2  31627  tendoconid  31640  tendotr  31641  cdlemk35s-id  31749  cdlemk39s-id  31751  cdlemk53b  31767  cdlemk53  31768  cdlemk54  31769  cdleml3N  31789  cdleml5N  31791  tendospcanN  31835  diclss  32005  dihvalcq2  32059  dihord4  32070  dihord5b  32071  dihord5apre  32074  dihmeetlem1N  32102  dihmeetbclemN  32116  dihmeetlem20N  32138  dihmeetALTN  32139  dihatlat  32146  dihatexv  32150  dochkr1  32290  dochkr1OLDN  32291  lcfl7lem  32311  lclkrlem2m  32331  hdmaplna1  32722  hdmaplns1  32723  hdmaplnm1  32724
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator