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

Theorem syl112anc 1222
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 532 . 2  |-  ( ph  ->  ( th  /\  ta ) )
6 syl112anc.5 . 2  |-  ( ( ps  /\  ch  /\  ( th  /\  ta )
)  ->  et )
71, 2, 5, 6syl3anc 1218 1  |-  ( ph  ->  et )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 371  df-3an 967
This theorem is referenced by:  fveqf1o  5995  enfixsn  7412  gruina  8977  grur1  8979  enqeq  9095  recrec  10020  rec11r  10022  divdivdiv  10024  dmdcan  10033  ddcan  10037  rereccl  10041  div2neg  10046  divmuld  10121  divmul2d  10132  divmul3d  10133  divassd  10134  div12d  10135  div23d  10136  divdird  10137  divsubdird  10138  div11d  10139  ltmul12a  10177  ltdiv1  10185  ltrec  10205  lt2msq1  10207  lediv2  10214  supmul1  10287  qbtwnre  11161  xlemul1a  11243  xlemul1  11245  xadd4d  11258  quoremz  11686  quoremnn0ALT  11688  expgt1  11894  nnlesq  11961  expnbnd  11985  expmulnbnd  11988  discr1  11992  facubnd  12068  hashf1lem1  12200  2swrdeqwrdeq  12339  sqrlem6  12729  mulcn2  13065  climcnds  13306  geomulcvg  13328  cvgrat  13335  eftlub  13385  eflegeo  13397  tanhlt1  13436  sin01bnd  13461  cos01bnd  13462  eirrlem  13478  bitsmod  13624  mulgcd  13722  prmind2  13766  mulgcddvds  13782  qnumgt0  13820  iserodd  13894  pcpremul  13902  fldivp1  13951  pcfaclem  13952  qexpz  13955  prmpwdvds  13957  pockthg  13959  prmreclem1  13969  prmreclem5  13973  4sqlem10  14000  4sqlem12  14009  4sqlem16  14013  4sqlem17  14014  vdwlem3  14036  vdwlem8  14041  vdwlem9  14042  0ram  14073  ramz2  14077  xpsc0  14490  xpsc1  14491  odmulg  16048  dfod2  16056  odf1o1  16062  odf1o2  16063  sylow3lem4  16120  ablsub4  16293  odadd1  16321  odadd2  16322  ablfacrp2  16556  ablfac1b  16559  ablfac1eu  16562  pgpfac1lem3a  16565  pgpfaclem2  16571  chrcong  17935  znrrg  17973  cygznlem1  17974  txdis  19180  txdis1cn  19183  ptunhmeo  19356  divstgplem  19666  blcld  20055  nlmvscnlem2  20241  blcvx  20350  metds0  20401  metdseq0  20405  icopnfcnv  20489  lebnumii  20513  ipcau2  20724  tchcphlem1  20725  ipcnlem2  20731  csbren  20873  trirn  20874  dyadf  21046  dyadovol  21048  dyaddisjlem  21050  dyadmaxlem  21052  opnmbllem  21056  mbfmulc2lem  21100  mbfi1fseqlem4  21171  mbfi1fseqlem5  21172  mbfi1fseqlem6  21173  itg2mulclem  21199  itg2monolem1  21203  itg2monolem3  21205  itg2cnlem2  21215  itgabs  21287  dvlip  21440  dvlt0  21452  dvcvx  21467  ftc1lem4  21486  dgrcolem2  21716  aaliou3lem2  21784  aaliou3lem9  21791  itgulm  21848  radcnvlem1  21853  abelthlem2  21872  abelthlem7  21878  tangtx  21942  cosne0  21961  cosordlem  21962  tanord1  21968  logdivlti  22044  logcnlem4  22065  logf1o2  22070  cxpcn3lem  22160  cxpaddle  22165  ang180lem2  22181  atanlogsublem  22285  atantan  22293  atanbndlem  22295  atans2  22301  leibpi  22312  log2tlbnd  22315  birthdaylem3  22322  efrlim  22338  jensenlem2  22356  ftalem1  22385  ftalem5  22389  basellem1  22393  basellem4  22396  fsumdvdsdiaglem  22498  dvdsflf1o  22502  fsumfldivdiaglem  22504  ppiub  22518  mersenne  22541  dchrptlem1  22578  bposlem1  22598  bposlem2  22599  bposlem4  22601  lgsdilem  22636  lgseisenlem1  22663  lgseisenlem2  22664  lgseisenlem3  22665  lgsquadlem1  22668  lgsquadlem2  22669  2sqlem3  22680  2sqlem8  22686  2sqlem11  22689  2sqblem  22691  chebbnd1lem2  22694  chebbnd1lem3  22695  rplogsumlem1  22708  rplogsumlem2  22709  dchrisumlem1  22713  dchrmusum2  22718  dchrisum0flblem1  22732  mulog2sumlem1  22758  logdivbnd  22780  pntpbnd1a  22809  pntpbnd1  22810  pntpbnd2  22811  pntlemh  22823  pntlemr  22826  pntlemk  22830  pntlemo  22831  ostth2lem1  22842  ostth2lem2  22858  ostth2lem3  22859  ostth3  22862  tglineinteq  23018  axsegcon  23124  axpaschlem  23137  vdgrun  23522  vdgrfiun  23523  eupath2lem3  23551  gxmodid  23717  nmbdoplbi  25379  nmcoplbi  25383  nmophmi  25386  nmbdfnlbi  25404  nmcfnlbi  25407  cnlnadjlem7  25428  nmopcoi  25450  resf1o  25981  xdivrec  26053  unitdivcld  26283  measvunilem  26578  measvuni  26580  measssd  26581  measiuns  26583  measinblem  26586  measdivcst  26591  oddpwdc  26689  probun  26754  totprobd  26761  dstrvprob  26806  zetacvg  26953  subfaclim  27028  conpcon  27076  cvmliftlem2  27127  cvmliftlem6  27131  cvmliftlem7  27132  cvmliftlem8  27133  cvmliftlem9  27134  cvmliftlem10  27135  snmlff  27170  lineext  28058  hilbert1.1  28136  opnmbllem0  28380  ismblfin  28385  itgabsnc  28414  ftc1cnnclem  28418  nn0prpwlem  28470  bfplem1  28674  bfp  28676  eldioph2lem1  29051  fphpdo  29109  irrapxlem1  29116  irrapxlem2  29117  irrapxlem3  29118  irrapxlem5  29120  pellexlem2  29124  pell1234qrreccl  29148  pell1234qrmulcl  29149  pell1234qrdich  29155  pell1qr1  29165  pellqrexplicit  29171  pellfundex  29180  reglogltb  29185  reglogleb  29186  pellfund14  29192  rmspecsqrnq  29200  rmxycomplete  29211  jm2.24nn  29255  jm2.17b  29257  jm2.17c  29258  jm2.18  29290  jm2.19lem2  29292  jm2.20nn  29299  jm2.16nn0  29306  jm3.1lem2  29320  areaquad  29545  stoweidlem1  29749  stoweidlem11  29759  stoweidlem14  29762  stoweidlem26  29774  stoweidlem34  29782  stoweidlem38  29786  stoweidlem60  29808  clwwlkf1  30411  domnmsuppn0  30733  lincvalpr  30841  ldepspr  30896  islindeps2  30906  lfl1  32555  lfladdcl  32556  eqlkr  32584  lkrlsp  32587  atcvrj2b  32916  3dim1  32951  3dim2  32952  llni2  32996  2llnjaN  33050  lvoli3  33061  lvoli2  33065  lncvrelatN  33265  lhpat4N  33528  lhpat3  33530  4atexlemex6  33558  ldilco  33600  ltrnid  33619  ltrnatb  33621  ltrnel  33623  ltrncnvel  33626  ltrncnv  33630  ltrn11at  33631  ltrneq  33633  ltrnmw  33635  trlat  33653  trlator0  33655  ltrnnidn  33658  trlid0  33660  trlnidatb  33661  trlnle  33670  trlval3  33671  trlval4  33672  cdlemc2  33676  cdlemc5  33679  cdlemc6  33680  cdlemc  33681  cdlemd2  33683  cdlemd9  33690  cdleme0e  33701  cdleme02N  33706  cdleme0ex1N  33707  cdleme3e  33716  cdleme3g  33718  cdleme3h  33719  cdleme3  33721  cdleme7aa  33726  cdleme7b  33728  cdleme7c  33729  cdleme7d  33730  cdleme7e  33731  cdleme7ga  33732  cdleme7  33733  cdleme9  33737  cdleme16aN  33743  cdleme11c  33745  cdleme11dN  33746  cdleme11e  33747  cdleme11h  33750  cdleme11j  33751  cdleme11k  33752  cdleme12  33755  cdleme21j  33820  cdleme26eALTN  33845  cdleme26f  33847  cdleme26f2  33849  cdlemefrs29bpre0  33880  cdleme35a  33932  cdleme35b  33934  cdleme35c  33935  cdleme35f  33938  cdleme36a  33944  cdleme38m  33947  cdlemeg46rgv  34012  cdlemeg46req  34013  cdlemf  34047  cdlemg2fvlem  34078  cdlemg2l  34087  cdlemg7N  34110  cdlemg12g  34133  cdlemg15  34140  cdlemg17h  34152  cdlemg17  34161  cdlemg19a  34167  cdlemg24  34172  cdlemg37  34173  cdlemg27a  34176  cdlemg31b0N  34178  cdlemg27b  34180  cdlemg31c  34183  cdlemg31d  34184  cdlemg35  34197  trljco  34224  tgrpgrplem  34233  cdlemh2  34300  tendoconid  34313  tendotr  34314  cdlemk35s-id  34422  cdlemk39s-id  34424  cdlemk53b  34440  cdlemk53  34441  cdlemk54  34442  cdleml3N  34462  cdleml5N  34464  tendospcanN  34508  diclss  34678  dihvalcq2  34732  dihord4  34743  dihord5b  34744  dihord5apre  34747  dihmeetlem1N  34775  dihmeetbclemN  34789  dihmeetlem20N  34811  dihmeetALTN  34812  dihatlat  34819  dihatexv  34823  dochkr1  34963  dochkr1OLDN  34964  lcfl7lem  34984  lclkrlem2m  35004  hdmaplna1  35395  hdmaplns1  35396  hdmaplnm1  35397
  Copyright terms: Public domain W3C validator