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

Theorem syl31anc 1221
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 )
syl31anc.5  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ta )  ->  et )
Assertion
Ref Expression
syl31anc  |-  ( ph  ->  et )

Proof of Theorem syl31anc
StepHypRef Expression
1 sylXanc.1 . . 3  |-  ( ph  ->  ps )
2 sylXanc.2 . . 3  |-  ( ph  ->  ch )
3 sylXanc.3 . . 3  |-  ( ph  ->  th )
41, 2, 33jca 1168 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
5 sylXanc.4 . 2  |-  ( ph  ->  ta )
6 syl31anc.5 . 2  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ta )  ->  et )
74, 5, 6syl2anc 661 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:  syl32anc  1226  thema4b  1585  smo11  6817  omeulem2  7014  oeeui  7033  oaabs2  7076  omabs  7078  omxpenlem  7404  map2xp  7473  mapdom2  7474  fsuppsssupp  7628  cantnflt  7872  cantnfltOLD  7902  cnfcom  7925  cnfcomOLD  7933  mapcdaen  8345  pwsdompw  8365  cofsmo  8430  fin1a2lem4  8564  ltmul12a  10177  lt2msq1  10207  ledivp1  10226  lemul1ad  10264  lemul2ad  10265  supmul1  10287  supmul  10290  rpnnen1lem3  10973  rpnnen1lem5  10975  lediv2ad  11041  xaddge0  11213  xadddi  11250  xadddi2  11252  supicc  11425  supiccub  11426  supicclub  11427  flval3  11655  modidmul0  11726  fseqsupubi  11792  expcan  11908  ltexp2  11909  ltexp2r  11912  expubnd  11916  ltexp2rd  12024  ltexp2d  12029  leexp2d  12030  expcand  12031  swrdid  12313  swrd0fv  12327  swrds1  12337  ccatswrd  12342  swrdccat2  12344  swrdccatin2  12370  swrdccatin12lem2  12372  swrdccatin12lem3  12373  splfv1  12389  cshwidxmod  12432  o1fsum  13268  mertenslem1  13336  eftlub  13385  rpnnen2lem4  13492  ruclem12  13515  dvdsadd  13563  3dvds  13588  divalgmod  13602  bitsmod  13624  bitsinv1lem  13629  bezoutlem4  13717  gcdeq  13728  rplpwr  13732  sqgcd  13734  rpmulgcd2  13783  isprm5  13790  divgcdodd  13797  rpdvds  13802  divnumden  13818  crt  13845  phimullem  13846  modprm0  13865  modprmn0modprm0  13867  coprimeprodsq2  13869  pythagtriplem19  13892  pockthlem  13958  prmunb  13967  prmreclem3  13971  prmreclem6  13974  ramub  14066  ramz  14078  pmtrprfv  15950  pmtrprfv3  15951  mndodcong  16036  odngen  16067  pgpfi  16095  pgpssslw  16104  sylow2blem3  16112  lsmless1  16149  lsmless2  16150  lsmless12  16151  lsmmod2  16164  pj1id  16187  odadd2  16322  gexexlem  16325  ablfacrplem  16554  ablfacrp  16555  ablfac1b  16559  ablfac1eu  16562  pgpfac1lem2  16564  lsmssspx  17146  lspsncv0  17204  coe1subfv  17695  znunit  17971  uvcvvcl2  18188  uvcvv1  18189  uvcvv0  18190  mdetunilem2  18394  clsndisj  18654  neiptopnei  18711  rnelfm  19501  fmfnfmlem2  19503  fmfnfm  19506  flimss1  19521  isfcf  19582  cnextfun  19611  cnextfvval  19612  cnextf  19613  cnextcn  19614  cnextfres  19615  ustuqtop1  19791  utopsnneiplem  19797  xblss2ps  19951  xblss2  19952  stdbdxmet  20065  metcnpi3  20096  metustexhalfOLD  20113  metustexhalf  20114  nmoi  20282  nmoi2  20284  nmoco  20291  blcvx  20350  icccmplem2  20375  icccmplem3  20376  reconnlem2  20379  xrge0gsumle  20385  metds0  20401  metdstri  20402  metdseq0  20405  lebnumlem3  20510  nmoleub2lem  20644  bcthlem5  20814  minveclem2  20888  minveclem3b  20890  minveclem4  20894  minveclem6  20896  icombl  21020  cncombf  21111  mbflimsup  21119  itg2monolem1  21203  itg2mono  21206  itg2cnlem1  21214  itg2cnlem2  21215  bddmulibl  21291  ellimc2  21327  cpnord  21384  cpnres  21386  dvmulbr  21388  dvcobr  21395  dvlipcn  21441  dvlip2  21442  c1liplem1  21443  dvivthlem1  21455  lhop1lem  21460  lhop1  21461  dvfsumlem2  21474  itgsubstlem  21495  deg1add  21550  deg1sublt  21557  ply1remlem  21609  plyeq0lem  21653  taylthlem2  21814  ulmdvlem3  21842  abelthlem7  21878  pilem2  21892  pilem3  21893  pige3  21954  logccv  22083  cxpaddlelem  22164  cvxcl  22353  fsumharmonic  22380  ftalem5  22389  dvdsdivcl  22496  dvdsmulf1o  22509  bposlem1  22598  lgsqr  22660  lgsquad2lem2  22673  2sqlem8a  22685  2sqlem8  22686  dchrmusum2  22718  dchrvmasumiflem1  22725  dchrisum0flblem1  22732  dchrisum0lem1b  22739  pntlem3  22833  axsegcon  23124  ax5seglem1  23125  ax5seglem2  23126  axlowdimlem6  23144  axeuclidlem  23159  axcontlem7  23167  axcontlem9  23169  axcontlem10  23170  cusgrasize2inds  23336  vdgrun  23522  vdgrfiun  23523  vdgr1d  23524  vdgr1b  23525  vdgr1a  23527  nmoub3i  24124  ubthlem3  24224  minvecolem2  24227  minvecolem4  24232  minvecolem5  24233  minvecolem6  24234  htthlem  24270  pjpjpre  24773  chscllem1  24991  chscllem2  24992  chscllem3  24993  cnlnadjlem2  25423  leopnmid  25493  br8d  25893  ogrpaddlt  26132  archirngz  26157  ornglmullt  26226  orngrmullt  26227  elrhmunit  26239  kerf1hrm  26243  qqhval2lem  26362  qqhnm  26371  qqhucn  26373  esumcst  26466  esumpcvgval  26479  measunl  26582  dya2iocbrsiga  26642  dya2icobrsiga  26643  sibfof  26678  oddpwdc  26689  eulerpartlemgc  26697  bayesth  26774  erdszelem8  27038  br8  27517  supaddc  28370  supadd  28371  totbndbnd  28641  prdsbnd  28645  rrncmslem  28684  rrntotbnd  28688  isdrngo2  28717  mzpsubst  29038  rencldnfi  29113  irrapx1  29122  pellexlem3  29125  pellexlem5  29127  infmrgelbi  29172  pellqrex  29173  pellfundge  29176  rmspecfund  29203  congtr  29261  acongeq  29279  bezoutr  29281  jm2.20nn  29299  jm2.25lem1  29300  jm2.26  29304  expdiophlem1  29323  hbtlem2  29433  stoweidlem1  29749  stoweidlem20  29768  stoweidlem24  29772  stoweidlem34  29782  stoweidlem45  29793  stoweidlem60  29808  elovmpt3rab1  30116  usgra2adedgspth  30258  difelfznle  30441  2pthfrgra  30556  vdn1frgrav2  30571  vdgn1frgrav2  30572  frgrawopreg  30595  frrusgraord  30617  numclwwlk2lem1  30648  numclwwlk3  30655  frgrareg  30663  pmatcollpw2lem  30820  lincresunit3  30904  lsatcmp  32488  lcvexchlem2  32520  lcvexchlem3  32521  ncvr1  32757  cvrletrN  32758  cvrnbtwn3  32761  cvrnrefN  32767  cvrcmp  32768  0ltat  32776  atnle0  32794  atlen0  32795  cvlcvr1  32824  cvrval3  32897  atle  32920  athgt  32940  1cvratex  32957  ps-2  32962  ps-2b  32966  llnnleat  32997  2atneat  32999  llnle  33002  atcvrlln  33004  llncmp  33006  2llnmat  33008  2at0mat0  33009  2atm  33011  ps-2c  33012  lplnle  33024  lplnnle2at  33025  llncvrlpln2  33041  llncvrlpln  33042  2lplnmN  33043  2llnmj  33044  2atmat  33045  lplncmp  33046  lplnexllnN  33048  2llnm2N  33052  2llnm4  33054  lvolnle3at  33066  4atlem3a  33081  4atlem3b  33082  4atlem10  33090  4atlem11  33093  4atlem12  33096  lplncvrlvol2  33099  lplncvrlvol  33100  lvolcmp  33101  2lplnm2N  33105  2lplnmj  33106  dalempjsen  33137  dalemcea  33144  dalem2  33145  dalemdea  33146  dalem9  33156  dalem16  33163  dalemcjden  33176  dalem21  33178  dalem23  33180  dalem39  33195  dalem54  33210  dalem60  33216  cdlemb  33278  elpadd2at  33290  paddasslem4  33307  paddasslem7  33310  paddasslem15  33318  paddasslem16  33319  pmodlem1  33330  pmodlem2  33331  llnexchb2  33353  pclfinclN  33434  osumcllem9N  33448  pmapojoinN  33452  pexmidN  33453  pl42lem1N  33463  lhp0lt  33487  lhpexle1  33492  lhpexle2lem  33493  lhpexle3lem  33495  lhprelat3N  33524  ltrnid  33619  trlval3  33671  arglem1N  33674  cdlemc5  33679  cdleme3b  33713  cdleme3c  33714  cdleme3h  33719  cdleme7e  33731  cdleme7ga  33732  cdleme20l1  33804  cdleme20l2  33805  cdleme20l  33806  cdleme22b  33825  cdlemefrs29clN  33883  cdlemefrs32fva  33884  cdlemeg46fvcl  33990  cdlemeg46c  33997  cdlemeg46fvaw  34000  cdlemeg46req  34013  cdleme48fgv  34022  cdlemf1  34045  cdlemg1cex  34072  cdlemg2dN  34074  cdlemg2ce  34076  cdlemg12e  34131  cdlemg35  34197  cdlemh  34301  tendocan  34308  cdlemk28-3  34392  tendoex  34459  dih1  34771  dihmeetlem9N  34800  dihlspsnssN  34817  dihlspsnat  34818  lcfrlem23  35050
  Copyright terms: Public domain W3C validator