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

Theorem syl21anc 1225
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 532 . 2  |-  ( ph  ->  ( ( ps  /\  ch )  /\  th )
)
5 syl21anc.4 . 2  |-  ( ( ( ps  /\  ch )  /\  th )  ->  ta )
64, 5syl 16 1  |-  ( ph  ->  ta )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
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 369
This theorem is referenced by:  wereu2  4865  brcogw  5160  funprg  5619  funtpg  5620  fnunsn  5670  fresaun  5738  fvun1  5919  iinpreima  5993  ftpg  6057  fsnunf  6085  soisores  6198  isotr  6207  off  6527  caofrss  6546  caonncan  6551  fvmpt2curryd  6992  oaf1o  7204  omeulem1  7223  oeordi  7228  oelimcl  7241  oeeulem  7242  oeeui  7243  oaabs2  7286  omabs  7288  pmresg  7439  ralxpmap  7461  domunsncan  7610  mapunen  7679  sucdom2  7707  unxpdom2  7721  sucxpdom  7722  ac6sfi  7756  unblem4  7767  fodomfi  7791  hartogslem1  7959  brwdom2  7991  cantnflt  8082  cantnflem3  8101  cantnflem4  8102  cantnfltOLD  8112  cantnflem3OLD  8123  cantnflem4OLD  8124  cnfcomlem  8134  cnfcom  8135  cnfcomlemOLD  8142  cnfcomOLD  8143  infxpenlem  8382  infxpenc  8386  infxpencOLD  8391  fseqenlem1  8396  pwsdompw  8575  cfeq0  8627  cofsmo  8640  cfsmolem  8641  ssfin4  8681  hsmexlem4  8800  hsmexlem5  8801  axdc3lem2  8822  axdc3lem4  8824  fpwwe2  9010  wunpr  9076  mulclpi  9260  mulcanenq  9327  distrlem4pr  9393  prlem934  9400  prlem936  9414  divge0d  11295  fseq1p1m1  11756  elfznelfzob  11897  seqcaopr2  12125  facavg  12361  hashimarn  12480  cats1un  12692  f1oun2prg  12856  sqrtdiv  13181  sqrtdivd  13337  mulcn2  13500  o1of2  13517  fsumsplit  13644  sumsplit  13665  isumless  13739  demoivreALT  14018  rpnnen2lem11  14042  qredeu  14332  isprm5  14337  rpexp  14345  rpdvds  14349  divnumden  14365  divdenle  14366  phimullem  14393  pythagtriplem4  14427  pythagtriplem8  14431  pythagtriplem9  14432  pcgcd1  14484  sumhash  14499  fldivp1  14500  pockthlem  14507  ssc2  15310  estrreslem1  15605  mndpropd  16145  grpidssd  16313  grpinvssd  16314  issubg2  16415  isnsg3  16434  eqgid  16452  gass  16538  symgextres  16649  gsmsymgreqlem2  16655  sylow1lem5  16821  sylow2alem2  16837  sylow3lem3  16848  efgredlemd  16961  efgredlem  16964  frgpnabllem1  17076  frgpnabllem2  17077  subgdmdprd  17276  ablfacrplem  17311  kerf1hrm  17587  issrngd  17705  lmodprop2d  17767  lsspropd  17858  pwssplit1  17900  lspvadd  17937  mplsubglem  18288  mplsubglemOLD  18290  mplind  18362  znidomb  18773  znrrg  18777  lindfind  19018  lindsind  19019  mat1ghm  19152  mdetunilem1  19281  mdetunilem3  19283  mdetunilem4  19284  mdetunilem9  19289  cramerimplem2  19353  mat2pmatlin  19403  monmatcollpw  19447  cpmadugsumlemF  19544  mretopd  19760  neiptopnei  19800  neitr  19848  ufilen  20597  flimrest  20650  flimclslem  20651  fclsrest  20691  cnextcn  20733  haustsms2  20801  tsmsxplem2  20822  trust  20898  utoptop  20903  restutop  20906  ustuqtop4  20913  utopsnneiplem  20916  utop2nei  20919  utop3cls  20920  isucn2  20948  ucnima  20950  ucncn  20954  fmucnd  20961  trcfilu  20963  comet  21182  metustexhalfOLD  21232  metustexhalf  21233  metustOLD  21236  metust  21237  metustblOLD  21249  metustbl  21250  metutopOLD  21251  psmetutop  21252  nrmmetd  21261  reconnlem1  21497  reconnlem2  21498  fsumcn  21540  cmetcaulem  21893  iscmet3lem1  21896  iscmet3lem2  21897  bcthlem5  21933  rrxdstprj1  22002  minveclem4  22013  ovolfiniun  22078  itg1addlem4  22272  itg1addlem5  22273  itgsplitioo  22410  c1liplem1  22563  dvfsumlem1  22593  plyeq0lem  22773  quotcan  22871  psercnlem1  22986  cxplea  23245  birthdaylem3  23481  musumsum  23666  dvdsmulf1o  23668  dchrelbas4  23716  dchrhash  23744  2sqlem8a  23844  2sqlem8  23845  chto1ub  23859  vmadivsum  23865  dchrisumlem1  23872  dchrvmasumlem2  23881  dchrvmasumiflem1  23884  rpvmasum2  23895  mulog2sumlem2  23918  selberg2lem  23933  pntrmax  23947  pntpbnd1  23969  pntlemb  23980  pntlemj  23986  ercgrg  24109  motcgr  24124  tglineeltr  24212  colline  24231  miriso  24251  midexlem  24270  perpneq  24292  foot  24297  f1otrg  24376  f1otrge  24377  axcontlem9  24477  uhgraun  24513  umgraun  24530  2wlklemA  24758  2wlklemB  24759  2wlklemC  24760  constr3trllem3  24854  vdgrun  25103  vdgrfiun  25104  eupap1  25178  nmblolbii  25912  minvecolem3  25990  minvecolem4  25994  htthlem  26032  bcs2  26297  nmopub2tALT  27026  nmfnleub2  27043  eighmorth  27081  nmophmi  27148  nmopcoadji  27218  hstle  27347  atcvat3i  27513  disjxpin  27658  off2  27702  xppreima2  27709  fgreu  27740  1stpreimas  27752  padct  27776  resf1o  27784  fpwrelmap  27787  xrofsup  27816  eliccelico  27822  elicoelioo  27823  iocinif  27826  difioo  27827  gcdnncl  27841  2sqcoprm  27869  2sqmod  27870  ressprs  27877  tleile  27883  xrge0addgt0  27915  xrge0adddir  27916  omndmul3  27937  archirng  27966  archirngz  27967  gsumle  28004  orngmul  28028  qtophaus  28074  locfinref  28079  metideq  28107  sqsscirc2  28126  tpr2rico  28129  fmcncfil  28148  lmxrge0  28169  lmdvg  28170  qqhval2lem  28196  qqhf  28201  qqhnm  28205  esumle  28287  gsumesum  28288  esumlef  28291  esumrnmpt2  28297  esumpcvgval  28307  esum2d  28322  ofcf  28332  imambfm  28470  omssubadd  28508  inelcarsg  28519  carsgsigalem  28523  carsggect  28526  carsgclctunlem2  28527  oddpwdc  28557  eulerpartlems  28563  eulerpartlemb  28571  eulerpartlemt  28574  iwrdsplit  28590  sseqfn  28593  sseqf  28595  sseqfres  28596  ballotlemfc0  28695  ballotlemfcc  28696  ballotlemfrcn0  28732  sgnsub  28747  plymulx0  28768  signsplypnf  28771  signsvtn0  28791  signstfvneq0  28793  signsvtp  28804  signsvtn  28805  cvxscon  28952  elmrsubrn  29144  nobndup  29700  nobnddown  29701  mblfinlem3  30293  itg2addnclem3  30308  ftc1cnnclem  30328  neibastop3  30420  mapfzcons  30888  mzpcl34  30903  mzpindd  30918  mzpsubst  30920  diophrw  30931  diophren  30986  irrapxlem1  30997  pellexlem5  31008  acongrep  31157  pwssplit4  31274  phisum  31400  mulltgt0  31637  fnchoice  31644  3adantlr3  31657  3adantll2  31660  3adantll3  31661  fmuldfeq  31816  mccl  31845  limccog  31865  limcrecl  31874  lptioo1  31877  islpcn  31884  limsupre  31886  neglimc  31892  0ellimcdiv  31894  limclner  31896  icccncfext  31929  fprodcncf  31943  dvnmptdivc  31974  dvnmul  31979  dvmptfprod  31981  dvnprodlem3  31984  stoweidlem25  32046  stoweidlem34  32055  stoweidlem38  32059  stoweidlem44  32065  stoweidlem48  32069  stoweidlem49  32070  stoweidlem59  32080  stoweidlem60  32081  wallispilem4  32089  stirlinglem5  32099  dirkercncflem2  32125  fourierdlem39  32167  fourierdlem42  32170  fourierdlem46  32174  fourierdlem47  32175  fourierdlem48  32176  fourierdlem50  32178  fourierdlem51  32179  fourierdlem64  32192  fourierdlem73  32201  fourierdlem74  32202  fourierdlem77  32205  fourierdlem80  32208  fourierdlem87  32215  fourierdlem94  32222  fourierdlem103  32231  fourierdlem104  32232  etransclem32  32288  uhgun  32752  lincresunit2  33333  nnpw2pmod  33458  dignn0flhalflem1  33490  dignn0flhalf  33493  4an4132  33655  bnj927  34228  bnj1536  34313  bnj1001  34417  bnj1280  34477  lautlt  36212  lautcvr  36213  lauteq  36216  lautco  36218  ltrncl  36246  ltrncnvleN  36251  trljat2  36289  cdlemc6  36318  cdleme20c  36434  cdleme20j  36441  cdleme22e  36467  cdleme22eALTN  36468  cdlemg7aN  36748  cdlemg12e  36770  cdlemg17dALTN  36787  cdlemh  36940  cdlemkfid1N  37044  dibglbN  37290  diblss  37294  diclspsn  37318  dih1  37410  dihglbcpreN  37424  dihmeetlem4preN  37430  lcfrlem19  37685
  Copyright terms: Public domain W3C validator