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

Theorem syl21anc 1181
Description: Syllogism combined with contraction. (Contributed by Jeff Hankins, 1-Aug-2009.)
Hypotheses
Ref Expression
sylXanc.1  |-  ( ph  ->  ps )
sylXanc.2  |-  ( ph  ->  ch )
sylXanc.3  |-  ( ph  ->  th )
syl21anc.4  |-  ( ( ( ps  /\  ch )  /\  th )  ->  ta )
Assertion
Ref Expression
syl21anc  |-  ( ph  ->  ta )

Proof of Theorem syl21anc
StepHypRef Expression
1 sylXanc.1 . . 3  |-  ( ph  ->  ps )
2 sylXanc.2 . . 3  |-  ( ph  ->  ch )
3 sylXanc.3 . . 3  |-  ( ph  ->  th )
41, 2, 3jca31 520 . 2  |-  ( ph  ->  ( ( ps  /\  ch )  /\  th )
)
5 syl21anc.4 . 2  |-  ( ( ( ps  /\  ch )  /\  th )  ->  ta )
64, 5syl 15 1  |-  ( ph  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  wereu2  4406  funprg  5317  fnunsn  5367  fresaun  5428  fvun1  5606  iinpreima  5671  fsnunf  5734  soisores  5840  isotr  5849  off  6109  caofrss  6126  caonncan  6131  oaf1o  6577  omeulem1  6596  oeordi  6601  oelimcl  6614  oeeulem  6615  oeeui  6616  oaabs2  6659  omabs  6661  pmresg  6811  domunsncan  6978  mapunen  7046  sucdom2  7073  unxpdom2  7087  sucxpdom  7088  ac6sfi  7117  unblem4  7128  fodomfi  7151  hartogslem1  7273  brwdom2  7303  cantnflt  7389  cantnflem3  7409  cantnflem4  7410  cnfcomlem  7418  cnfcom  7419  infxpenlem  7657  infxpenc  7661  fseqenlem1  7667  pwsdompw  7846  cfeq0  7898  cofsmo  7911  cfsmolem  7912  ssfin4  7952  hsmexlem4  8071  hsmexlem5  8072  axdc3lem2  8093  axdc3lem4  8095  fpwwe2  8281  wunpr  8347  mulclpi  8533  mulcanenq  8600  distrlem4pr  8666  prlem934  8673  prlem936  8687  divge0d  10442  fseq1p1m1  10873  seqcaopr2  11098  facavg  11330  cats1un  11492  sqrdiv  11767  sqrdivd  11922  mulcn2  12085  o1of2  12102  fsumsplit  12228  sumsplit  12247  isumless  12320  demoivreALT  12497  rpnnen2lem11  12519  qredeu  12802  isprm5  12807  rpexp  12815  rpdvds  12819  divnumden  12835  divdenle  12836  phimullem  12863  pythagtriplem4  12888  pythagtriplem8  12892  pythagtriplem9  12893  pcgcd1  12945  sumhash  12960  fldivp1  12961  pockthlem  12968  ssc2  13715  mndpropd  14414  issubg2  14652  isnsg3  14667  eqgid  14685  gass  14771  sylow1lem5  14929  sylow2alem2  14945  sylow3lem3  14956  efgredlemd  15069  efgredlem  15072  frgpnabllem1  15177  frgpnabllem2  15178  subgdmdprd  15285  ablfacrplem  15316  issrngd  15642  lmodprop2d  15703  lsspropd  15790  lspvadd  15865  mplsubglem  16195  mplind  16259  znidomb  16531  znrrg  16535  mretopd  16845  ufilen  17641  flimrest  17694  flimclslem  17695  fclsrest  17735  haustsms2  17835  tsmsxplem2  17852  comet  18075  nrmmetd  18113  reconnlem1  18347  reconnlem2  18348  fsumcn  18390  cmetcaulem  18730  iscmet3lem1  18733  iscmet3lem2  18734  bcthlem5  18766  bcth2  18768  minveclem4  18812  ovolfiniun  18876  itg1addlem4  19070  itg1addlem5  19071  itgsplitioo  19208  c1liplem1  19359  dvfsumlem1  19389  plyeq0lem  19608  quotcan  19705  psercnlem1  19817  cxplea  20059  birthdaylem3  20264  musumsum  20448  dvdsmulf1o  20450  dchrelbas4  20498  dchrhash  20526  2sqlem8a  20626  2sqlem8  20627  chto1ub  20641  vmadivsum  20647  dchrisumlem1  20654  dchrvmasumlem2  20663  dchrvmasumiflem1  20666  rpvmasum2  20677  mulog2sumlem2  20700  selberg2lem  20715  pntrmax  20729  pntpbnd1  20751  pntlemb  20762  pntlemj  20768  nmblolbii  21393  minvecolem3  21471  minvecolem4  21475  htthlem  21513  bcs2  21777  nmopub2tALT  22505  nmfnleub2  22522  eighmorth  22560  nmophmi  22627  nmopcoadji  22697  hstle  22826  atcvat3i  22992  ballotlemsgt1  23085  ballotlemfrcn0  23104  off2  23223  xppreima2  23227  eliccelico  23285  elicoelioo  23286  iocinif  23289  difioo  23290  sqsscirc2  23308  tpr2rico  23311  xrge0addgt0  23346  xrge0adddir  23347  lmxrge0  23390  lmdvg  23391  esumle  23448  esumlef  23450  esumpcvgval  23461  ofcf  23479  imambfm  23582  cvxscon  23789  umgraun  23894  vdgrun  23908  eupap1  23915  nobndup  24425  nobnddown  24426  axcontlem9  24672  clscnc  26113  isig2a2  26169  neibastop3  26414  ralxpmap  26864  mapfzcons  26896  mzpcl34  26912  mzpindd  26927  mzpsubst  26929  diophrw  26941  diophren  26999  irrapxlem1  27010  pellexlem5  27021  acongrep  27170  pwssplit1  27291  pwssplit4  27294  lindfind  27389  lindsind  27390  phisum  27621  f1oun2prg  28187  uslgraun  28254  constr3trllem3  28398  bnj927  29116  bnj1536  29202  bnj1001  29306  bnj1280  29366  lautlt  30902  lautcvr  30903  lauteq  30906  lautco  30908  ltrncl  30936  ltrncnvleN  30941  trljat2  30978  cdlemc6  31007  cdleme20c  31122  cdleme20j  31129  cdleme22e  31155  cdleme22eALTN  31156  cdlemg7aN  31436  cdlemg12e  31458  cdlemg17dALTN  31475  cdlemh  31628  cdlemkfid1N  31732  dibglbN  31978  diblss  31982  diclspsn  32006  dih1  32098  dihglbcpreN  32112  dihmeetlem4preN  32118  lcfrlem19  32373
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
  Copyright terms: Public domain W3C validator