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

Theorem syl21anc 1267
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 537 . 2  |-  ( ph  ->  ( ( ps  /\  ch )  /\  th )
)
5 syl21anc.4 . 2  |-  ( ( ( ps  /\  ch )  /\  th )  ->  ta )
64, 5syl 17 1  |-  ( ph  ->  ta )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371
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 189  df-an 373
This theorem is referenced by:  wereu2  4831  brcogw  5003  funprg  5631  funtpg  5632  fnunsn  5683  fresaun  5754  fvun1  5936  iinpreima  6010  ftpg  6074  fsnunf  6102  f1prex  6182  soisores  6218  isotr  6227  off  6546  caofrss  6564  caonncan  6569  fvmpt2curryd  7018  oaf1o  7264  omeulem1  7283  oeordi  7288  oelimcl  7301  oeeulem  7302  oeeui  7303  oaabs2  7346  omabs  7348  pmresg  7499  ralxpmap  7521  domunsncan  7672  mapunen  7741  sucdom2  7768  unxpdom2  7780  sucxpdom  7781  ac6sfi  7815  unblem4  7826  fodomfi  7850  hartogslem1  8057  brwdom2  8088  cantnflt  8177  cantnflem3  8196  cantnflem4  8197  cnfcomlem  8204  cnfcom  8205  infxpenlem  8444  infxpenc  8449  fseqenlem1  8455  pwsdompw  8634  cfeq0  8686  cofsmo  8699  cfsmolem  8700  ssfin4  8740  hsmexlem4  8859  hsmexlem5  8860  axdc3lem2  8881  axdc3lem4  8883  fpwwe2  9068  wunpr  9134  mulclpi  9318  mulcanenq  9385  distrlem4pr  9451  prlem934  9458  prlem936  9472  divge0d  11378  fseq1p1m1  11868  elfznelfzob  12015  seqcaopr2  12249  facavg  12486  hashimarn  12610  cats1un  12832  f1oun2prg  13002  sqrtdiv  13329  sqrtdivd  13485  mulcn2  13659  o1of2  13676  fsumsplit  13806  sumsplit  13829  isumless  13903  demoivreALT  14255  rpnnen2lem11  14277  gcdnncl  14481  isprm5  14651  qredeu  14664  rpexp  14672  rpdvds  14676  divnumden  14697  divdenle  14698  phimullem  14727  pythagtriplem4  14769  pythagtriplem8  14773  pythagtriplem9  14774  pcgcd1  14826  sumhash  14841  fldivp1  14842  pockthlem  14849  ssc2  15727  estrreslem1  16022  mndpropd  16562  grpidssd  16730  grpinvssd  16731  issubg2  16832  isnsg3  16851  eqgid  16869  gass  16955  symgextres  17066  gsmsymgreqlem2  17072  sylow1lem5  17254  sylow2alem2  17270  sylow3lem3  17281  efgredlemd  17394  efgredlem  17397  frgpnabllem1  17509  frgpnabllem2  17510  subgdmdprd  17667  ablfacrplem  17698  kerf1hrm  17971  issrngd  18089  lmodprop2d  18150  lsspropd  18240  pwssplit1  18282  lspvadd  18319  mplsubglem  18658  mplind  18725  znidomb  19132  znrrg  19136  lindfind  19374  lindsind  19375  mat1ghm  19508  mdetunilem1  19637  mdetunilem3  19639  mdetunilem4  19640  mdetunilem9  19645  cramerimplem2  19709  mat2pmatlin  19759  monmatcollpw  19803  cpmadugsumlemF  19900  mretopd  20108  neiptopnei  20148  neitr  20196  ufilen  20945  flimrest  20998  flimclslem  20999  fclsrest  21039  cnextcn  21082  haustsms2  21151  tsmsxplem2  21168  trust  21244  utoptop  21249  restutop  21252  ustuqtop4  21259  utopsnneiplem  21262  utop2nei  21265  utop3cls  21266  isucn2  21294  ucnima  21296  ucncn  21300  fmucnd  21307  trcfilu  21309  comet  21528  metustexhalf  21571  metust  21573  metustbl  21581  psmetutop  21582  nrmmetd  21589  reconnlem1  21844  reconnlem2  21845  fsumcn  21902  cmetcaulem  22258  iscmet3lem1  22261  iscmet3lem2  22262  bcthlem5  22296  rrxdstprj1  22363  minveclem4  22374  minveclem4OLD  22386  ovolfiniun  22454  itg1addlem4  22657  itg1addlem5  22658  itgsplitioo  22795  c1liplem1  22948  dvfsumlem1  22978  plyeq0lem  23164  quotcan  23262  psercnlem1  23380  cxplea  23641  birthdaylem3  23879  musumsum  24121  dvdsmulf1o  24123  dchrelbas4  24171  dchrhash  24199  2sqlem8a  24299  2sqlem8  24300  chto1ub  24314  vmadivsum  24320  dchrisumlem1  24327  dchrvmasumlem2  24336  dchrvmasumiflem1  24339  rpvmasum2  24350  mulog2sumlem2  24373  selberg2lem  24388  pntrmax  24402  pntpbnd1  24424  pntlemb  24435  pntlemj  24441  ercgrg  24562  tgcgr4  24576  motcgr  24581  tglineeltr  24676  colline  24694  miriso  24715  midexlem  24737  perpneq  24759  foot  24764  f1otrg  24901  f1otrge  24902  axcontlem9  25002  uhgraun  25038  umgraun  25055  2wlklemA  25284  2wlklemB  25285  2wlklemC  25286  constr3trllem3  25380  vdgrun  25629  vdgrfiun  25630  eupap1  25704  nmblolbii  26440  minvecolem3  26518  minvecolem4  26522  minvecolem3OLD  26528  minvecolem4OLD  26532  htthlem  26570  bcs2  26835  nmopub2tALT  27562  nmfnleub2  27579  eighmorth  27617  nmophmi  27684  nmopcoadji  27754  hstle  27883  atcvat3i  28049  disjxpin  28198  off2  28242  xppreima2  28249  fgreu  28274  1stpreimas  28286  padct  28307  resf1o  28315  fpwrelmap  28318  xrofsup  28353  eliccelico  28359  elicoelioo  28360  iocinif  28363  difioo  28364  2sqcoprm  28408  2sqmod  28409  ressprs  28416  tleile  28422  xrge0addgt0  28454  xrge0adddir  28455  omndmul3  28476  archirng  28505  archirngz  28506  gsumle  28542  orngmul  28566  1smat1  28630  madjusmdetlem2  28654  qtophaus  28663  locfinref  28668  metideq  28696  sqsscirc2  28715  tpr2rico  28718  fmcncfil  28737  lmxrge0  28758  lmdvg  28759  qqhval2lem  28785  qqhf  28790  qqhnm  28794  esumle  28879  gsumesum  28880  esumlef  28883  esumrnmpt2  28889  esumpcvgval  28899  esum2d  28914  ofcf  28924  ldsysgenld  28982  ldgenpisyslem1  28985  unelros  28993  difelros  28994  inelsros  29000  diffiunisros  29001  imambfm  29084  omssubadd  29128  omssubaddOLD  29132  inelcarsg  29143  carsgsigalem  29147  carsggect  29150  carsgclctunlem2  29151  oddpwdc  29187  eulerpartlems  29193  eulerpartlemb  29201  eulerpartlemt  29204  iwrdsplit  29220  sseqfn  29223  sseqf  29225  sseqfres  29226  ballotlemfc0  29325  ballotlemfcc  29326  ballotlemfrcn0  29362  ballotlemfrcn0OLD  29400  sgnsub  29415  plymulx0  29436  signsplypnf  29439  signsvtn0  29459  signstfvneq0  29461  signsvtp  29472  signsvtn  29473  bnj927  29580  bnj1536  29665  bnj1001  29769  bnj1280  29829  cvxscon  29966  elmrsubrn  30158  nobndup  30589  nobnddown  30590  neibastop3  31018  finxpsuclem  31789  poimirlem16  31956  poimirlem19  31959  poimirlem20  31960  poimirlem29  31969  mblfinlem3  31979  itg2addnclem3  31995  ftc1cnnclem  32015  lautlt  33656  lautcvr  33657  lauteq  33660  lautco  33662  ltrncl  33690  ltrncnvleN  33695  trljat2  33733  cdlemc6  33762  cdleme20c  33878  cdleme20j  33885  cdleme22e  33911  cdleme22eALTN  33912  cdlemg7aN  34192  cdlemg12e  34214  cdlemg17dALTN  34231  cdlemh  34384  cdlemkfid1N  34488  dibglbN  34734  diblss  34738  diclspsn  34762  dih1  34854  dihglbcpreN  34868  dihmeetlem4preN  34874  lcfrlem19  35129  mapfzcons  35558  mzpcl34  35573  mzpindd  35588  mzpsubst  35590  diophrw  35601  diophren  35656  irrapxlem1  35666  pellexlem5  35677  acongrep  35830  pwssplit4  35947  phisum  36076  brtrclfv2  36319  4an4132  36855  mulltgt0  37343  fnchoice  37350  3adantlr3  37362  3adantll2  37364  3adantll3  37365  uzwo4  37392  disjf1o  37466  supxrgelem  37560  fmuldfeq  37661  mccl  37678  limccog  37700  limcrecl  37709  lptioo1  37712  islpcn  37719  limsupre  37721  limsupreOLD  37722  neglimc  37728  0ellimcdiv  37730  limclner  37732  icccncfext  37765  fprodcncf  37779  dvnmptdivc  37813  dvnmul  37818  dvmptfprod  37820  dvnprodlem3  37823  stoweidlem25  37885  stoweidlem34  37895  stoweidlem38  37899  stoweidlem44  37905  stoweidlem48  37909  stoweidlem49  37910  stoweidlem59  37920  stoweidlem60  37921  wallispilem4  37930  stirlinglem5  37940  dirkercncflem2  37966  fourierdlem39  38009  fourierdlem42  38012  fourierdlem42OLD  38013  fourierdlem46  38016  fourierdlem47  38017  fourierdlem48  38018  fourierdlem50  38020  fourierdlem51  38021  fourierdlem64  38034  fourierdlem73  38043  fourierdlem74  38044  fourierdlem77  38047  fourierdlem80  38050  fourierdlem87  38057  fourierdlem94  38064  fourierdlem103  38073  fourierdlem104  38074  etransclem32  38131  sge0cl  38223  sge0f1o  38224  nnfoctbdjlem  38293  ismeannd  38305  omeiunltfirp  38340  hoicvr  38370  ovncvrrp  38386  hoidmvlelem2  38418  hoidmvlelem5  38421  hspdifhsp  38438  hoiqssbllem2  38445  hspmbllem2  38449  fdisjdmun  38630  uspgr1ewop  39323  nbupgrres  39438  uhgun  39745  lincresunit2  40324  nnpw2pmod  40447  dignn0flhalflem1  40479  dignn0flhalf  40482
  Copyright terms: Public domain W3C validator