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

Theorem syl21anc 857
Description: Syllogism combined with contraction. (Contributed by Jeff Hankins, 1-Aug-2009.)
Hypotheses
Ref Expression
syl12anc.1 (𝜑𝜓)
syl12anc.2 (𝜑𝜒)
syl12anc.3 (𝜑𝜃)
syl21anc.4 (((𝜓𝜒) ∧ 𝜃) → 𝜏)
Assertion
Ref Expression
syl21anc (𝜑𝜏)

Proof of Theorem syl21anc
StepHypRef Expression
1 syl12anc.1 . . 3 (𝜑𝜓)
2 syl12anc.2 . . 3 (𝜑𝜒)
3 syl12anc.3 . . 3 (𝜑𝜃)
41, 2, 3jca31 506 . 2 (𝜑 → ((𝜓𝜒) ∧ 𝜃))
5 syl21anc.4 . 2 (((𝜓𝜒) ∧ 𝜃) → 𝜏)
64, 5syl 17 1 (𝜑𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 198  df-an 385
This theorem is referenced by:  wereu2  5308  funtpg  6155  funcnvtp  6163  funcnvqp  6164  fnunsn  6209  fun2d  6283  fresaun  6290  fvun1  6490  iinpreima  6567  ftpg  6647  fsnunf  6676  f1prex  6763  soisores  6801  isotr  6810  off  7142  caofrss  7160  caonncan  7165  fvmpt2curryd  7632  oaf1o  7880  omeulem1  7899  oeordi  7904  oelimcl  7917  oeeulem  7918  oeeui  7919  oaabs2  7962  omabs  7964  pmresg  8120  ralxpmap  8144  domunsncan  8299  mapunen  8368  sucdom2  8395  unxpdom2  8407  sucxpdom  8408  ac6sfi  8443  unblem4  8454  fodomfi  8478  hartogslem1  8686  brwdom2  8717  cantnflt  8816  cantnflem3  8835  cantnflem4  8836  cnfcomlem  8843  cnfcom  8844  infxpenlem  9119  infxpenc  9124  fseqenlem1  9130  pwsdompw  9311  cfeq0  9363  cofsmo  9376  cfsmolem  9377  ssfin4  9417  hsmexlem4  9536  hsmexlem5  9537  axdc3lem2  9558  axdc3lem4  9560  fpwwe2  9750  wunpr  9816  mulclpi  10000  mulcanenq  10067  distrlem4pr  10133  prlem934  10140  prlem936  10154  divge0d  12126  fseq1p1m1  12637  elfznelfzob  12798  seqcaopr2  13060  facavg  13308  cats1un  13699  f1oun2prg  13886  sqrtdiv  14229  sqrtdivd  14385  mulcn2  14549  o1of2  14566  fsumsplit  14694  sumsplit  14722  isumless  14799  demoivreALT  15151  rpnnen2lem11  15173  gcdnncl  15448  qredeu  15590  rpdvds  15592  isprm5  15636  rpexp  15649  divnumden  15673  divdenle  15674  phimullem  15701  phisum  15712  pythagtriplem4  15741  pythagtriplem8  15745  pythagtriplem9  15746  pcgcd1  15798  sumhash  15817  fldivp1  15818  pockthlem  15826  setsfun  16104  setsfun0  16105  ssc2  16686  estrreslem1  16981  mndpropd  17521  grpidssd  17696  grpinvssd  17697  issubg2  17811  isnsg3  17830  eqgid  17848  gass  17935  symgextres  18046  gsmsymgreqlem2  18052  sylow1lem5  18218  sylow2alem2  18234  sylow3lem3  18245  efgredlemd  18358  efgredlem  18361  frgpnabllem1  18477  frgpnabllem2  18478  subgdmdprd  18635  ablfacrplem  18666  kerf1hrm  18947  issrngd  19065  lmodprop2d  19129  lsspropd  19224  pwssplit1  19266  lspvadd  19303  mplsubglem  19643  mplind  19710  znidomb  20117  znrrg  20121  lindfind  20365  lindsind  20366  mat1ghm  20500  mdetunilem1  20629  mdetunilem3  20631  mdetunilem4  20632  mdetunilem9  20637  cramerimplem2  20703  mat2pmatlin  20753  monmatcollpw  20797  cpmadugsumlemF  20894  mretopd  21110  neiptopnei  21150  neitr  21198  ufilen  21947  flimrest  22000  flimclslem  22001  fclsrest  22041  cnextcn  22084  haustsms2  22153  tsmsxplem2  22170  trust  22246  utoptop  22251  restutop  22254  ustuqtop4  22261  utopsnneiplem  22264  utop2nei  22267  utop3cls  22268  isucn2  22296  ucnima  22298  ucncn  22302  fmucnd  22309  trcfilu  22311  comet  22531  metustexhalf  22574  metustbl  22584  psmetutop  22585  nrmmetd  22592  reconnlem1  22842  reconnlem2  22843  fsumcn  22886  cmetcaulem  23298  iscmet3lem1  23301  iscmet3lem2  23302  bcthlem5  23337  rrxdstprj1  23404  minveclem4  23415  ovolfiniun  23482  itg1addlem4  23680  itg1addlem5  23681  itgsplitioo  23818  c1liplem1  23973  dvfsumlem1  24003  plyeq0lem  24180  quotcan  24278  psercnlem1  24393  cxplea  24656  birthdaylem3  24894  musumsum  25132  dvdsmulf1o  25134  dchrelbas4  25182  dchrhash  25210  gausslemma2dlem0d  25298  gausslemma2dlem1a  25304  2lgslem1a1  25328  2sqlem8a  25364  2sqlem8  25365  chto1ub  25379  vmadivsum  25385  dchrisumlem1  25392  dchrvmasumlem2  25401  dchrvmasumiflem1  25404  rpvmasum2  25415  mulog2sumlem2  25438  selberg2lem  25453  pntrmax  25467  pntpbnd1  25489  pntlemb  25500  pntlemj  25506  ercgrg  25626  tgcgr4  25640  motcgr  25645  tglineeltr  25740  colline  25758  miriso  25779  midexlem  25801  perpneq  25823  foot  25828  f1otrg  25965  f1otrge  25966  axcontlem9  26066  uspgr1ewop  26356  nbupgrres  26481  structtocusgr  26570  wlkp1  26806  clwlkl1loop  26907  uspgrn2crct  26929  crctcshwlkn0lem5  26935  3trlond  27346  3pthond  27348  3spthond  27350  frgr3v  27450  vdgn1frgrv2  27471  numclwwlk3  27573  nmblolbii  27982  minvecolem3  28060  minvecolem4  28064  htthlem  28102  bcs2  28367  nmopub2tALT  29096  nmfnleub2  29113  eighmorth  29151  nmophmi  29218  nmopcoadji  29288  hstle  29417  atcvat3i  29583  disjxpin  29726  fmptco1f1o  29761  off2  29770  xppreima2  29777  fgreu  29798  1stpreimas  29810  padct  29824  resf1o  29832  fpwrelmap  29835  xrofsup  29860  eliccelico  29866  elicoelioo  29867  iocinif  29870  difioo  29871  2sqcoprm  29972  2sqmod  29973  ressprs  29980  tleile  29986  xrge0addgt0  30016  xrge0adddir  30017  omndmul3  30038  archirng  30067  archirngz  30068  gsumle  30104  orngmul  30128  1smat1  30195  madjusmdetlem2  30219  qtophaus  30228  locfinref  30233  metideq  30261  sqsscirc2  30280  tpr2rico  30283  fmcncfil  30302  lmxrge0  30323  lmdvg  30324  qqhval2lem  30350  qqhf  30355  qqhnm  30359  esumle  30445  gsumesum  30446  esumlef  30449  esumrnmpt2  30455  esumpcvgval  30465  esum2d  30480  ofcf  30490  ldsysgenld  30548  ldgenpisyslem1  30551  unelros  30559  difelros  30560  inelsros  30566  diffiunisros  30567  imambfm  30649  omssubadd  30687  inelcarsg  30698  carsgsigalem  30702  carsggect  30705  carsgclctunlem2  30706  oddpwdc  30741  eulerpartlems  30747  eulerpartlemb  30755  eulerpartlemt  30758  iwrdsplit  30774  sseqfn  30777  sseqf  30779  sseqfres  30780  ballotlemfc0  30879  ballotlemfcc  30880  ballotlemfrcn0  30916  sgnsub  30931  plymulx0  30949  signsplypnf  30952  signsvtn0  30972  signstfvneq0  30974  signsvtp  30985  signsvtn  30986  fsum2dsub  31010  reprlt  31022  hashreprin  31023  reprgt  31024  reprpmtf1o  31029  chtvalz  31032  breprexplema  31033  breprexplemc  31035  breprexp  31036  circlemeth  31043  logdivsqrle  31053  hgt750lemb  31059  bnj927  31162  bnj1536  31247  bnj1001  31351  bnj1280  31411  cvxsconn  31548  elmrsubrn  31740  frpomin  32059  noextend  32140  neibastop3  32678  finxpsuclem  33550  poimirlem16  33738  poimirlem19  33741  poimirlem20  33742  poimirlem29  33751  mblfinlem3  33761  itg2addnclem3  33775  ftc1cnnclem  33795  lautlt  35871  lautcvr  35872  lauteq  35875  lautco  35877  ltrncl  35905  ltrncnvleN  35910  trljat2  35948  cdlemc6  35977  cdleme20c  36092  cdleme20j  36099  cdleme22e  36125  cdleme22eALTN  36126  cdlemg7aN  36406  cdlemg12e  36428  cdlemg17dALTN  36445  cdlemh  36598  cdlemkfid1N  36702  dibglbN  36947  diblss  36951  diclspsn  36975  dih1  37067  dihglbcpreN  37081  dihmeetlem4preN  37087  lcfrlem19  37342  mapfzcons  37781  mzpcl34  37796  mzpindd  37811  mzpsubst  37813  diophrw  37824  diophren  37879  irrapxlem1  37888  pellexlem5  37899  acongrep  38048  pwssplit4  38160  brtrclfv2  38519  rfovcnvf1od  38798  ntrk0kbimka  38837  isotone1  38846  isotone2  38847  4an4132  39203  mulltgt0  39675  fnchoice  39682  3adantlr3  39694  3adantll2  39696  3adantll3  39697  uzwo4  39714  disjf1o  39867  supxrgelem  40033  infleinflem2  40067  xrralrecnnle  40082  supxrunb3  40102  unb2ltle  40121  infrpgernmpt  40174  iooiinicc  40249  iooiinioc  40263  fmuldfeq  40295  mccl  40310  limccog  40332  limcrecl  40341  lptioo1  40344  islpcn  40351  limsupre  40353  neglimc  40359  0ellimcdiv  40361  limclner  40363  climleltrp  40388  climinf3  40428  liminflimsupclim  40519  icccncfext  40580  fprodcncf  40594  dvnmptdivc  40633  dvnmul  40638  dvmptfprod  40640  dvnprodlem3  40643  stoweidlem25  40721  stoweidlem34  40730  stoweidlem38  40734  stoweidlem44  40740  stoweidlem48  40744  stoweidlem49  40745  stoweidlem59  40755  stoweidlem60  40756  wallispilem4  40764  stirlinglem5  40774  dirkercncflem2  40800  fourierdlem39  40842  fourierdlem42  40845  fourierdlem46  40848  fourierdlem47  40849  fourierdlem48  40850  fourierdlem50  40852  fourierdlem51  40853  fourierdlem64  40866  fourierdlem73  40875  fourierdlem74  40876  fourierdlem77  40879  fourierdlem80  40882  fourierdlem87  40889  fourierdlem94  40896  fourierdlem103  40905  fourierdlem104  40906  etransclem32  40962  rrxsnicc  40999  sge0cl  41077  sge0f1o  41078  nnfoctbdjlem  41151  ismeannd  41163  omeiunltfirp  41215  hoicvr  41244  ovncvrrp  41260  hoidmvlelem2  41292  hoidmvlelem5  41295  hspdifhsp  41312  hoiqssbllem2  41319  hspmbllem2  41323  vonicclem2  41380  smflimsuplem7  41514  sqrtpwpw2p  42025  lincresunit2  42835  nnpw2pmod  42945  dignn0flhalflem1  42977  dignn0flhalf  42980
  Copyright terms: Public domain W3C validator