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

Theorem syl21anc 1227
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 534 . 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 369
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
This theorem is referenced by:  wereu2  4876  brcogw  5171  funprg  5637  funtpg  5638  fnunsn  5688  fresaun  5756  fvun1  5938  iinpreima  6011  ftpg  6071  fsnunf  6099  soisores  6211  isotr  6220  off  6538  caofrss  6557  caonncan  6562  fvmpt2curryd  7000  oaf1o  7212  omeulem1  7231  oeordi  7236  oelimcl  7249  oeeulem  7250  oeeui  7251  oaabs2  7294  omabs  7296  pmresg  7446  ralxpmap  7468  domunsncan  7617  mapunen  7686  sucdom2  7714  unxpdom2  7728  sucxpdom  7729  ac6sfi  7764  unblem4  7775  fodomfi  7799  hartogslem1  7967  brwdom2  7999  cantnflt  8091  cantnflem3  8110  cantnflem4  8111  cantnfltOLD  8121  cantnflem3OLD  8132  cantnflem4OLD  8133  cnfcomlem  8143  cnfcom  8144  cnfcomlemOLD  8151  cnfcomOLD  8152  infxpenlem  8391  infxpenc  8395  infxpencOLD  8400  fseqenlem1  8405  pwsdompw  8584  cfeq0  8636  cofsmo  8649  cfsmolem  8650  ssfin4  8690  hsmexlem4  8809  hsmexlem5  8810  axdc3lem2  8831  axdc3lem4  8833  fpwwe2  9021  wunpr  9087  mulclpi  9271  mulcanenq  9338  distrlem4pr  9404  prlem934  9411  prlem936  9425  divge0d  11292  fseq1p1m1  11752  elfznelfzob  11884  seqcaopr2  12111  facavg  12347  hashimarn  12462  swrdspsleq  12636  cats1un  12664  f1oun2prg  12828  sqrtdiv  13062  sqrtdivd  13218  mulcn2  13381  o1of2  13398  fsumsplit  13525  sumsplit  13546  isumless  13620  demoivreALT  13797  rpnnen2lem11  13819  qredeu  14107  isprm5  14112  rpexp  14120  rpdvds  14124  divnumden  14140  divdenle  14141  phimullem  14168  pythagtriplem4  14202  pythagtriplem8  14206  pythagtriplem9  14207  pcgcd1  14259  sumhash  14274  fldivp1  14275  pockthlem  14282  ssc2  15052  mndpropd  15764  grpidssd  15924  grpinvssd  15925  issubg2  16021  isnsg3  16040  eqgid  16058  gass  16144  symgextres  16255  gsmsymgreqlem2  16261  sylow1lem5  16428  sylow2alem2  16444  sylow3lem3  16455  efgredlemd  16568  efgredlem  16571  frgpnabllem1  16680  frgpnabllem2  16681  subgdmdprd  16883  ablfacrplem  16918  kerf1hrm  17192  issrngd  17310  lmodprop2d  17372  lsspropd  17463  pwssplit1  17505  lspvadd  17542  mplsubglem  17892  mplsubglemOLD  17894  mplind  17966  znidomb  18395  znrrg  18399  lindfind  18646  lindsind  18647  mat1ghm  18780  mdetunilem1  18909  mdetunilem3  18911  mdetunilem4  18912  mdetunilem9  18917  cramerimplem2  18981  mat2pmatlin  19031  monmatcollpw  19075  cpmadugsumlemF  19172  mretopd  19387  neiptopnei  19427  neitr  19475  ufilen  20194  flimrest  20247  flimclslem  20248  fclsrest  20288  cnextcn  20330  haustsms2  20398  tsmsxplem2  20419  trust  20495  utoptop  20500  restutop  20503  ustuqtop4  20510  utopsnneiplem  20513  utop2nei  20516  utop3cls  20517  isucn2  20545  ucnima  20547  ucncn  20551  fmucnd  20558  trcfilu  20560  comet  20779  metustexhalfOLD  20829  metustexhalf  20830  metustOLD  20833  metust  20834  metustblOLD  20846  metustbl  20847  metutopOLD  20848  psmetutop  20849  nrmmetd  20858  reconnlem1  21094  reconnlem2  21095  fsumcn  21137  cmetcaulem  21490  iscmet3lem1  21493  iscmet3lem2  21494  bcthlem5  21530  rrxdstprj1  21599  minveclem4  21610  ovolfiniun  21675  itg1addlem4  21869  itg1addlem5  21870  itgsplitioo  22007  c1liplem1  22160  dvfsumlem1  22190  plyeq0lem  22370  quotcan  22467  psercnlem1  22582  cxplea  22833  birthdaylem3  23039  musumsum  23224  dvdsmulf1o  23226  dchrelbas4  23274  dchrhash  23302  2sqlem8a  23402  2sqlem8  23403  chto1ub  23417  vmadivsum  23423  dchrisumlem1  23430  dchrvmasumlem2  23439  dchrvmasumiflem1  23442  rpvmasum2  23453  mulog2sumlem2  23476  selberg2lem  23491  pntrmax  23505  pntpbnd1  23527  pntlemb  23538  pntlemj  23544  ercgrg  23664  motcgr  23679  tglineeltr  23753  colline  23771  miriso  23791  midexlem  23805  perpneq  23827  foot  23832  f1otrg  23878  f1otrge  23879  axcontlem9  23979  uhgraun  24015  umgraun  24032  2wlklemA  24260  2wlklemB  24261  2wlklemC  24262  constr3trllem3  24356  vdgrun  24605  vdgrfiun  24606  eupap1  24680  nmblolbii  25418  minvecolem3  25496  minvecolem4  25500  htthlem  25538  bcs2  25803  nmopub2tALT  26532  nmfnleub2  26549  eighmorth  26587  nmophmi  26654  nmopcoadji  26724  hstle  26853  atcvat3i  27019  disjxpin  27148  off2  27182  xppreima2  27188  fgreu  27213  resf1o  27253  fpwrelmap  27256  xrofsup  27278  eliccelico  27284  elicoelioo  27285  iocinif  27288  difioo  27289  ressprs  27333  tleile  27339  toslublem  27345  tosglblem  27347  xrge0addgt0  27371  xrge0adddir  27372  omndmul2  27392  omndmul3  27393  archirng  27422  archirngz  27423  archiabl  27432  gsumle  27461  orngmul  27484  ofldchr  27495  metideq  27536  pstmxmet  27540  sqsscirc2  27555  tpr2rico  27558  fmcncfil  27577  lmxrge0  27598  lmdvg  27599  qqhval2lem  27626  qqhf  27631  qqhnm  27635  qtophaus  27665  esumle  27733  gsumesum  27735  esumlef  27738  esumpcvgval  27752  ofcf  27770  imambfm  27901  oddpwdc  27961  eulerpartlems  27967  eulerpartlemb  27975  eulerpartlemt  27978  iwrdsplit  27994  sseqfn  27997  sseqf  27999  sseqfres  28000  ballotlemfc0  28099  ballotlemfcc  28100  ballotlemfrcn0  28136  sgncl  28145  sgnsub  28151  plymulx0  28172  signsplypnf  28175  signsvtn0  28195  signstfvneq0  28197  signsvtp  28208  signsvtn  28209  signlem0  28212  cvxscon  28356  nobndup  29065  nobnddown  29066  mblfinlem3  29658  itg2addnclem3  29673  ftc1cnnclem  29693  neibastop3  29811  mapfzcons  30280  mzpcl34  30295  mzpindd  30310  mzpsubst  30313  diophrw  30324  diophren  30379  irrapxlem1  30390  pellexlem5  30401  acongrep  30550  pwssplit4  30667  phisum  30792  mulltgt0  31003  fnchoice  31010  3adantlr3  31023  3adantll2  31027  3adantll3  31028  fmuldfeq  31161  islpcn  31209  limsupre  31211  limclner  31221  stoweidlem25  31353  stoweidlem34  31362  stoweidlem38  31366  stoweidlem44  31372  stoweidlem48  31376  stoweidlem49  31377  stoweidlem59  31387  stoweidlem60  31388  wallispilem4  31396  stirlinglem5  31406  fourierdlem9  31444  fourierdlem31  31466  fourierdlem39  31474  fourierdlem42  31477  fourierdlem46  31481  fourierdlem47  31482  fourierdlem48  31483  fourierdlem50  31485  fourierdlem51  31486  fourierdlem64  31499  fourierdlem71  31506  fourierdlem73  31508  fourierdlem74  31509  fourierdlem77  31512  fourierdlem80  31515  fourierdlem87  31522  fourierdlem94  31529  fourierdlem95  31530  fourierdlem103  31538  fourierdlem104  31539  fourierdlem113  31548  uhgun  31875  lincresunit2  32178  bnj927  32924  bnj1536  33009  bnj1001  33113  bnj1280  33173  lautlt  34905  lautcvr  34906  lauteq  34909  lautco  34911  ltrncl  34939  ltrncnvleN  34944  trljat2  34981  cdlemc6  35010  cdleme20c  35125  cdleme20j  35132  cdleme22e  35158  cdleme22eALTN  35159  cdlemg7aN  35439  cdlemg12e  35461  cdlemg17dALTN  35478  cdlemh  35631  cdlemkfid1N  35735  dibglbN  35981  diblss  35985  diclspsn  36009  dih1  36101  dihglbcpreN  36115  dihmeetlem4preN  36121  lcfrlem19  36376
  Copyright terms: Public domain W3C validator