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

Theorem syl21anc 1317
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 555 . 2 (𝜑 → ((𝜓𝜒) ∧ 𝜃))
5 syl21anc.4 . 2 (((𝜓𝜒) ∧ 𝜃) → 𝜏)
64, 5syl 17 1 (𝜑𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 196  df-an 385
This theorem is referenced by:  wereu2  5035  funprgOLD  5855  funtpg  5856  funtpgOLD  5857  funcnvtp  5865  funcnvqp  5866  funcnvqpOLD  5867  fnunsn  5912  fun2d  5981  fresaun  5988  fvun1  6179  iinpreima  6253  ftpg  6328  fsnunf  6356  f1prex  6439  soisores  6477  isotr  6486  off  6810  caofrss  6828  caonncan  6833  fvmpt2curryd  7284  oaf1o  7530  omeulem1  7549  oeordi  7554  oelimcl  7567  oeeulem  7568  oeeui  7569  oaabs2  7612  omabs  7614  pmresg  7771  ralxpmap  7793  domunsncan  7945  mapunen  8014  sucdom2  8041  unxpdom2  8053  sucxpdom  8054  ac6sfi  8089  unblem4  8100  fodomfi  8124  hartogslem1  8330  brwdom2  8361  cantnflt  8452  cantnflem3  8471  cantnflem4  8472  cnfcomlem  8479  cnfcom  8480  infxpenlem  8719  infxpenc  8724  fseqenlem1  8730  pwsdompw  8909  cfeq0  8961  cofsmo  8974  cfsmolem  8975  ssfin4  9015  hsmexlem4  9134  hsmexlem5  9135  axdc3lem2  9156  axdc3lem4  9158  fpwwe2  9344  wunpr  9410  mulclpi  9594  mulcanenq  9661  distrlem4pr  9727  prlem934  9734  prlem936  9748  divge0d  11788  fseq1p1m1  12283  elfznelfzob  12440  seqcaopr2  12699  facavg  12950  cats1un  13327  f1oun2prg  13512  sqrtdiv  13854  sqrtdivd  14010  mulcn2  14174  o1of2  14191  fsumsplit  14318  sumsplit  14341  isumless  14416  demoivreALT  14770  rpnnen2lem11  14792  gcdnncl  15067  qredeu  15210  rpdvds  15212  isprm5  15257  rpexp  15270  divnumden  15294  divdenle  15295  phimullem  15322  phisum  15333  pythagtriplem4  15362  pythagtriplem8  15366  pythagtriplem9  15367  pcgcd1  15419  sumhash  15438  fldivp1  15439  pockthlem  15447  setsfun  15725  setsfun0  15726  ssc2  16305  estrreslem1  16600  mndpropd  17139  grpidssd  17314  grpinvssd  17315  issubg2  17432  isnsg3  17451  eqgid  17469  gass  17557  symgextres  17668  gsmsymgreqlem2  17674  sylow1lem5  17840  sylow2alem2  17856  sylow3lem3  17867  efgredlemd  17980  efgredlem  17983  frgpnabllem1  18099  frgpnabllem2  18100  subgdmdprd  18256  ablfacrplem  18287  kerf1hrm  18566  issrngd  18684  lmodprop2d  18748  lsspropd  18838  pwssplit1  18880  lspvadd  18917  mplsubglem  19255  mplind  19323  znidomb  19729  znrrg  19733  lindfind  19974  lindsind  19975  mat1ghm  20108  mdetunilem1  20237  mdetunilem3  20239  mdetunilem4  20240  mdetunilem9  20245  cramerimplem2  20309  mat2pmatlin  20359  monmatcollpw  20403  cpmadugsumlemF  20500  mretopd  20706  neiptopnei  20746  neitr  20794  ufilen  21544  flimrest  21597  flimclslem  21598  fclsrest  21638  cnextcn  21681  haustsms2  21750  tsmsxplem2  21767  trust  21843  utoptop  21848  restutop  21851  ustuqtop4  21858  utopsnneiplem  21861  utop2nei  21864  utop3cls  21865  isucn2  21893  ucnima  21895  ucncn  21899  fmucnd  21906  trcfilu  21908  comet  22128  metustexhalf  22171  metustbl  22181  psmetutop  22182  nrmmetd  22189  reconnlem1  22437  reconnlem2  22438  fsumcn  22481  cmetcaulem  22894  iscmet3lem1  22897  iscmet3lem2  22898  bcthlem5  22933  rrxdstprj1  23000  minveclem4  23011  ovolfiniun  23076  itg1addlem4  23272  itg1addlem5  23273  itgsplitioo  23410  c1liplem1  23563  dvfsumlem1  23593  plyeq0lem  23770  quotcan  23868  psercnlem1  23983  cxplea  24242  birthdaylem3  24480  musumsum  24718  dvdsmulf1o  24720  dchrelbas4  24768  dchrhash  24796  gausslemma2dlem0d  24884  gausslemma2dlem1a  24890  2lgslem1a1  24914  2sqlem8a  24950  2sqlem8  24951  chto1ub  24965  vmadivsum  24971  dchrisumlem1  24978  dchrvmasumlem2  24987  dchrvmasumiflem1  24990  rpvmasum2  25001  mulog2sumlem2  25024  selberg2lem  25039  pntrmax  25053  pntpbnd1  25075  pntlemb  25086  pntlemj  25092  ercgrg  25212  tgcgr4  25226  motcgr  25231  tglineeltr  25326  colline  25344  miriso  25365  midexlem  25387  perpneq  25409  foot  25414  f1otrg  25551  f1otrge  25552  axcontlem9  25652  uhgraun  25840  umgraun  25857  2wlklemA  26084  2wlklemB  26085  2wlklemC  26086  constr3trllem3  26180  vdgrun  26428  vdgrfiun  26429  eupap1  26503  nmblolbii  27038  minvecolem3  27116  minvecolem4  27120  htthlem  27158  bcs2  27423  nmopub2tALT  28152  nmfnleub2  28169  eighmorth  28207  nmophmi  28274  nmopcoadji  28344  hstle  28473  atcvat3i  28639  disjxpin  28783  off2  28823  xppreima2  28830  fgreu  28854  1stpreimas  28866  padct  28885  resf1o  28893  fpwrelmap  28896  xrofsup  28923  eliccelico  28929  elicoelioo  28930  iocinif  28933  difioo  28934  2sqcoprm  28978  2sqmod  28979  ressprs  28986  tleile  28992  xrge0addgt0  29022  xrge0adddir  29023  omndmul3  29044  archirng  29073  archirngz  29074  gsumle  29110  orngmul  29134  1smat1  29198  madjusmdetlem2  29222  qtophaus  29231  locfinref  29236  metideq  29264  sqsscirc2  29283  tpr2rico  29286  fmcncfil  29305  lmxrge0  29326  lmdvg  29327  qqhval2lem  29353  qqhf  29358  qqhnm  29362  esumle  29447  gsumesum  29448  esumlef  29451  esumrnmpt2  29457  esumpcvgval  29467  esum2d  29482  ofcf  29492  ldsysgenld  29550  ldgenpisyslem1  29553  unelros  29561  difelros  29562  inelsros  29568  diffiunisros  29569  imambfm  29651  omssubadd  29689  inelcarsg  29700  carsgsigalem  29704  carsggect  29707  carsgclctunlem2  29708  oddpwdc  29743  eulerpartlems  29749  eulerpartlemb  29757  eulerpartlemt  29760  iwrdsplit  29776  sseqfn  29779  sseqf  29781  sseqfres  29782  ballotlemfc0  29881  ballotlemfcc  29882  ballotlemfrcn0  29918  sgnsub  29933  plymulx0  29950  signsplypnf  29953  signsvtn0  29973  signstfvneq0  29975  signsvtp  29986  signsvtn  29987  bnj927  30093  bnj1536  30178  bnj1001  30282  bnj1280  30342  cvxscon  30479  elmrsubrn  30671  nobndup  31099  nobnddown  31100  neibastop3  31527  finxpsuclem  32410  poimirlem16  32595  poimirlem19  32598  poimirlem20  32599  poimirlem29  32608  mblfinlem3  32618  itg2addnclem3  32633  ftc1cnnclem  32653  lautlt  34395  lautcvr  34396  lauteq  34399  lautco  34401  ltrncl  34429  ltrncnvleN  34434  trljat2  34472  cdlemc6  34501  cdleme20c  34617  cdleme20j  34624  cdleme22e  34650  cdleme22eALTN  34651  cdlemg7aN  34931  cdlemg12e  34953  cdlemg17dALTN  34970  cdlemh  35123  cdlemkfid1N  35227  dibglbN  35473  diblss  35477  diclspsn  35501  dih1  35593  dihglbcpreN  35607  dihmeetlem4preN  35613  lcfrlem19  35868  mapfzcons  36297  mzpcl34  36312  mzpindd  36327  mzpsubst  36329  diophrw  36340  diophren  36395  irrapxlem1  36404  pellexlem5  36415  acongrep  36565  pwssplit4  36677  brtrclfv2  37038  rfovcnvf1od  37318  ntrk0kbimka  37357  isotone1  37366  isotone2  37367  4an4132  37726  mulltgt0  38204  fnchoice  38211  3adantlr3  38223  3adantll2  38225  3adantll3  38226  uzwo4  38246  disjf1o  38373  supxrgelem  38494  infleinflem2  38528  xrralrecnnle  38543  iooiinicc  38616  iooiinioc  38630  fmuldfeq  38650  mccl  38665  limccog  38687  limcrecl  38696  lptioo1  38699  islpcn  38706  limsupre  38708  neglimc  38714  0ellimcdiv  38716  limclner  38718  climleltrp  38743  icccncfext  38773  fprodcncf  38787  dvnmptdivc  38828  dvnmul  38833  dvmptfprod  38835  dvnprodlem3  38838  stoweidlem25  38918  stoweidlem34  38927  stoweidlem38  38931  stoweidlem44  38937  stoweidlem48  38941  stoweidlem49  38942  stoweidlem59  38952  stoweidlem60  38953  wallispilem4  38961  stirlinglem5  38971  dirkercncflem2  38997  fourierdlem39  39039  fourierdlem42  39042  fourierdlem46  39045  fourierdlem47  39046  fourierdlem48  39047  fourierdlem50  39049  fourierdlem51  39050  fourierdlem64  39063  fourierdlem73  39072  fourierdlem74  39073  fourierdlem77  39076  fourierdlem80  39079  fourierdlem87  39086  fourierdlem94  39093  fourierdlem103  39102  fourierdlem104  39103  etransclem32  39159  rrxsnicc  39196  sge0cl  39274  sge0f1o  39275  nnfoctbdjlem  39348  ismeannd  39360  omeiunltfirp  39409  hoicvr  39438  ovncvrrp  39454  hoidmvlelem2  39486  hoidmvlelem5  39489  hspdifhsp  39506  hoiqssbllem2  39513  hspmbllem2  39517  vonicclem2  39575  sqrtpwpw2p  39988  uspgr1ewop  40474  nbupgrres  40592  1wlkp1  40890  clwlkl1loop  40989  uspgrn2crct  41011  crctcsh1wlkn0lem5  41017  3trlond  41340  3pthond  41342  3spthond  41344  frgr3v  41445  vdgn1frgrv2  41466  av-numclwwlk3  41539  lincresunit2  42061  nnpw2pmod  42175  dignn0flhalflem1  42207  dignn0flhalf  42210
  Copyright terms: Public domain W3C validator