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

Theorem syl21anc 1462
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 558 . 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 197  df-an 385
This theorem is referenced by:  wereu2  5251  funprgOLD  6090  funtpg  6091  funtpgOLD  6092  funcnvtp  6100  funcnvqp  6101  funcnvqpOLD  6102  fnunsn  6147  fun2d  6217  fresaun  6224  fvun1  6419  iinpreima  6496  ftpg  6574  fsnunf  6603  f1prex  6690  soisores  6728  isotr  6737  off  7065  caofrss  7083  caonncan  7088  fvmpt2curryd  7554  oaf1o  7800  omeulem1  7819  oeordi  7824  oelimcl  7837  oeeulem  7838  oeeui  7839  oaabs2  7882  omabs  7884  pmresg  8039  ralxpmap  8061  domunsncan  8213  mapunen  8282  sucdom2  8309  unxpdom2  8321  sucxpdom  8322  ac6sfi  8357  unblem4  8368  fodomfi  8392  hartogslem1  8600  brwdom2  8631  cantnflt  8730  cantnflem3  8749  cantnflem4  8750  cnfcomlem  8757  cnfcom  8758  infxpenlem  8997  infxpenc  9002  fseqenlem1  9008  pwsdompw  9189  cfeq0  9241  cofsmo  9254  cfsmolem  9255  ssfin4  9295  hsmexlem4  9414  hsmexlem5  9415  axdc3lem2  9436  axdc3lem4  9438  fpwwe2  9628  wunpr  9694  mulclpi  9878  mulcanenq  9945  distrlem4pr  10011  prlem934  10018  prlem936  10032  divge0d  12076  fseq1p1m1  12578  elfznelfzob  12739  seqcaopr2  13002  facavg  13253  cats1un  13646  f1oun2prg  13833  sqrtdiv  14176  sqrtdivd  14332  mulcn2  14496  o1of2  14513  fsumsplit  14641  sumsplit  14669  isumless  14747  demoivreALT  15101  rpnnen2lem11  15123  gcdnncl  15402  qredeu  15545  rpdvds  15547  isprm5  15592  rpexp  15605  divnumden  15629  divdenle  15630  phimullem  15657  phisum  15668  pythagtriplem4  15697  pythagtriplem8  15701  pythagtriplem9  15702  pcgcd1  15754  sumhash  15773  fldivp1  15774  pockthlem  15782  setsfun  16066  setsfun0  16067  ssc2  16654  estrreslem1  16949  mndpropd  17488  grpidssd  17663  grpinvssd  17664  issubg2  17781  isnsg3  17800  eqgid  17818  gass  17905  symgextres  18016  gsmsymgreqlem2  18022  sylow1lem5  18188  sylow2alem2  18204  sylow3lem3  18215  efgredlemd  18328  efgredlem  18331  frgpnabllem1  18447  frgpnabllem2  18448  subgdmdprd  18604  ablfacrplem  18635  kerf1hrm  18916  issrngd  19034  lmodprop2d  19098  lsspropd  19190  pwssplit1  19232  lspvadd  19269  mplsubglem  19607  mplind  19675  znidomb  20083  znrrg  20087  lindfind  20328  lindsind  20329  mat1ghm  20462  mdetunilem1  20591  mdetunilem3  20593  mdetunilem4  20594  mdetunilem9  20599  cramerimplem2  20663  mat2pmatlin  20713  monmatcollpw  20757  cpmadugsumlemF  20854  mretopd  21069  neiptopnei  21109  neitr  21157  ufilen  21906  flimrest  21959  flimclslem  21960  fclsrest  22000  cnextcn  22043  haustsms2  22112  tsmsxplem2  22129  trust  22205  utoptop  22210  restutop  22213  ustuqtop4  22220  utopsnneiplem  22223  utop2nei  22226  utop3cls  22227  isucn2  22255  ucnima  22257  ucncn  22261  fmucnd  22268  trcfilu  22270  comet  22490  metustexhalf  22533  metustbl  22543  psmetutop  22544  nrmmetd  22551  reconnlem1  22801  reconnlem2  22802  fsumcn  22845  cmetcaulem  23257  iscmet3lem1  23260  iscmet3lem2  23261  bcthlem5  23296  rrxdstprj1  23363  minveclem4  23374  ovolfiniun  23440  itg1addlem4  23636  itg1addlem5  23637  itgsplitioo  23774  c1liplem1  23929  dvfsumlem1  23959  plyeq0lem  24136  quotcan  24234  psercnlem1  24349  cxplea  24612  birthdaylem3  24850  musumsum  25088  dvdsmulf1o  25090  dchrelbas4  25138  dchrhash  25166  gausslemma2dlem0d  25254  gausslemma2dlem1a  25260  2lgslem1a1  25284  2sqlem8a  25320  2sqlem8  25321  chto1ub  25335  vmadivsum  25341  dchrisumlem1  25348  dchrvmasumlem2  25357  dchrvmasumiflem1  25360  rpvmasum2  25371  mulog2sumlem2  25394  selberg2lem  25409  pntrmax  25423  pntpbnd1  25445  pntlemb  25456  pntlemj  25462  ercgrg  25582  tgcgr4  25596  motcgr  25601  tglineeltr  25696  colline  25714  miriso  25735  midexlem  25757  perpneq  25779  foot  25784  f1otrg  25921  f1otrge  25922  axcontlem9  26022  uspgr1ewop  26310  nbupgrres  26435  structtocusgr  26523  wlkp1  26759  clwlkl1loop  26860  uspgrn2crct  26882  crctcshwlkn0lem5  26888  3trlond  27296  3pthond  27298  3spthond  27300  frgr3v  27400  vdgn1frgrv2  27421  numclwwlk3  27524  nmblolbii  27934  minvecolem3  28012  minvecolem4  28016  htthlem  28054  bcs2  28319  nmopub2tALT  29048  nmfnleub2  29065  eighmorth  29103  nmophmi  29170  nmopcoadji  29240  hstle  29369  atcvat3i  29535  disjxpin  29679  fmptco1f1o  29714  off2  29723  xppreima2  29730  fgreu  29751  1stpreimas  29763  padct  29777  resf1o  29785  fpwrelmap  29788  xrofsup  29813  eliccelico  29819  elicoelioo  29820  iocinif  29823  difioo  29824  2sqcoprm  29927  2sqmod  29928  ressprs  29935  tleile  29941  xrge0addgt0  29971  xrge0adddir  29972  omndmul3  29993  archirng  30022  archirngz  30023  gsumle  30059  orngmul  30083  1smat1  30150  madjusmdetlem2  30174  qtophaus  30183  locfinref  30188  metideq  30216  sqsscirc2  30235  tpr2rico  30238  fmcncfil  30257  lmxrge0  30278  lmdvg  30279  qqhval2lem  30305  qqhf  30310  qqhnm  30314  esumle  30400  gsumesum  30401  esumlef  30404  esumrnmpt2  30410  esumpcvgval  30420  esum2d  30435  ofcf  30445  ldsysgenld  30503  ldgenpisyslem1  30506  unelros  30514  difelros  30515  inelsros  30521  diffiunisros  30522  imambfm  30604  omssubadd  30642  inelcarsg  30653  carsgsigalem  30657  carsggect  30660  carsgclctunlem2  30661  oddpwdc  30696  eulerpartlems  30702  eulerpartlemb  30710  eulerpartlemt  30713  iwrdsplit  30729  sseqfn  30732  sseqf  30734  sseqfres  30735  ballotlemfc0  30834  ballotlemfcc  30835  ballotlemfrcn0  30871  sgnsub  30886  plymulx0  30904  signsplypnf  30907  signsvtn0  30927  signstfvneq0  30929  signsvtp  30940  signsvtn  30941  fsum2dsub  30965  reprlt  30977  hashreprin  30978  reprgt  30979  reprpmtf1o  30984  chtvalz  30987  breprexplema  30988  breprexplemc  30990  breprexp  30991  circlemeth  30998  logdivsqrle  31008  hgt750lemb  31014  bnj927  31117  bnj1536  31202  bnj1001  31306  bnj1280  31366  cvxsconn  31503  elmrsubrn  31695  frpomin  32015  noextend  32096  neibastop3  32634  finxpsuclem  33516  poimirlem16  33707  poimirlem19  33710  poimirlem20  33711  poimirlem29  33720  mblfinlem3  33730  itg2addnclem3  33745  ftc1cnnclem  33765  lautlt  35849  lautcvr  35850  lauteq  35853  lautco  35855  ltrncl  35883  ltrncnvleN  35888  trljat2  35926  cdlemc6  35955  cdleme20c  36070  cdleme20j  36077  cdleme22e  36103  cdleme22eALTN  36104  cdlemg7aN  36384  cdlemg12e  36406  cdlemg17dALTN  36423  cdlemh  36576  cdlemkfid1N  36680  dibglbN  36926  diblss  36930  diclspsn  36954  dih1  37046  dihglbcpreN  37060  dihmeetlem4preN  37066  lcfrlem19  37321  mapfzcons  37750  mzpcl34  37765  mzpindd  37780  mzpsubst  37782  diophrw  37793  diophren  37848  irrapxlem1  37857  pellexlem5  37868  acongrep  38018  pwssplit4  38130  brtrclfv2  38490  rfovcnvf1od  38769  ntrk0kbimka  38808  isotone1  38817  isotone2  38818  4an4132  39176  mulltgt0  39649  fnchoice  39656  3adantlr3  39668  3adantll2  39670  3adantll3  39671  uzwo4  39689  disjf1o  39846  supxrgelem  40020  infleinflem2  40054  xrralrecnnle  40069  supxrunb3  40090  unb2ltle  40109  infrpgernmpt  40162  iooiinicc  40241  iooiinioc  40255  fmuldfeq  40287  mccl  40302  limccog  40324  limcrecl  40333  lptioo1  40336  islpcn  40343  limsupre  40345  neglimc  40351  0ellimcdiv  40353  limclner  40355  climleltrp  40380  climinf3  40420  liminflimsupclim  40511  icccncfext  40572  fprodcncf  40586  dvnmptdivc  40625  dvnmul  40630  dvmptfprod  40632  dvnprodlem3  40635  stoweidlem25  40714  stoweidlem34  40723  stoweidlem38  40727  stoweidlem44  40733  stoweidlem48  40737  stoweidlem49  40738  stoweidlem59  40748  stoweidlem60  40749  wallispilem4  40757  stirlinglem5  40767  dirkercncflem2  40793  fourierdlem39  40835  fourierdlem42  40838  fourierdlem46  40841  fourierdlem47  40842  fourierdlem48  40843  fourierdlem50  40845  fourierdlem51  40846  fourierdlem64  40859  fourierdlem73  40868  fourierdlem74  40869  fourierdlem77  40872  fourierdlem80  40875  fourierdlem87  40882  fourierdlem94  40889  fourierdlem103  40898  fourierdlem104  40899  etransclem32  40955  rrxsnicc  40992  sge0cl  41070  sge0f1o  41071  nnfoctbdjlem  41144  ismeannd  41156  omeiunltfirp  41208  hoicvr  41237  ovncvrrp  41253  hoidmvlelem2  41285  hoidmvlelem5  41288  hspdifhsp  41305  hoiqssbllem2  41312  hspmbllem2  41316  vonicclem2  41373  smflimsuplem7  41507  sqrtpwpw2p  41929  lincresunit2  42746  nnpw2pmod  42856  dignn0flhalflem1  42888  dignn0flhalf  42891
  Copyright terms: Public domain W3C validator