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

Theorem syl21anc 835
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 (𝜑𝜒)
31, 2jca 514 . 2 (𝜑 → (𝜓𝜒))
4 syl12anc.3 . 2 (𝜑𝜃)
5 syl21anc.4 . 2 (((𝜓𝜒) ∧ 𝜃) → 𝜏)
63, 4, 5syl2anc 586 1 (𝜑𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398
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 209  df-an 399
This theorem is referenced by:  syl1111anc  837  wereu2  5547  funtpg  6404  funcnvtp  6412  funcnvqp  6413  fnunsn  6459  fun2d  6537  fvun1  6749  iinpreima  6832  ftpg  6913  fsnunf  6942  f1prex  7034  soisores  7074  isotr  7083  off  7418  caofrss  7436  caonncan  7441  fvmpocurryd  7931  oaf1o  8183  omeulem1  8202  oeordi  8207  oelimcl  8220  oeeulem  8221  oeeui  8222  oaabs2  8266  omabs  8268  pmresg  8428  ralxpmap  8454  domunsncan  8611  sucdom2  8708  unxpdom2  8720  sucxpdom  8721  unblem4  8767  fodomfi  8791  hartogslem1  9000  brwdom2  9031  cantnflt  9129  cantnflem3  9148  cantnflem4  9149  cnfcomlem  9156  cnfcom  9157  infxpenlem  9433  infxpenc  9438  fseqenlem1  9444  pwsdompw  9620  cfeq0  9672  cofsmo  9685  cfsmolem  9686  ssfin4  9726  hsmexlem4  9845  hsmexlem5  9846  axdc3lem2  9867  fpwwe2  10059  wunpr  10125  mulclpi  10309  mulcanenq  10376  distrlem4pr  10442  prlem934  10449  prlem936  10463  divge0d  12465  elfznelfzob  13137  seqcaopr2  13400  facavg  13655  swrdwrdsymb  14018  cats1un  14077  f1oun2prg  14273  sqrtdiv  14619  sqrtdivd  14777  mulcn2  14946  o1of2  14963  fsumsplit  15091  sumsplit  15117  isumless  15194  demoivreALT  15548  rpnnen2lem11  15571  gcdnncl  15850  qredeu  15996  rpdvds  15998  isprm5  16045  rpexp  16058  divnumden  16082  divdenle  16083  phimullem  16110  phisum  16121  pythagtriplem4  16150  pythagtriplem8  16154  pythagtriplem9  16155  pcgcd1  16207  sumhash  16226  fldivp1  16227  pockthlem  16235  setsfun  16512  setsfun0  16513  ssc2  17086  estrreslem1  17381  mndpropd  17930  grpidssd  18169  grpinvssd  18170  issubg2  18288  isnsg3  18306  eqgid  18326  gass  18425  symgextres  18547  gsmsymgreqlem2  18553  sylow1lem5  18721  sylow2alem2  18737  sylow3lem3  18748  efgredlemd  18864  efgredlem  18867  frgpnabllem1  18987  frgpnabllem2  18988  subgdmdprd  19150  ablfacrplem  19181  kerf1ghm  19491  kerf1hrmOLD  19492  issrngd  19626  lmodprop2d  19690  lsspropd  19783  pwssplit1  19825  lspvadd  19862  mplsubglem  20208  mplind  20276  znidomb  20702  znrrg  20706  lindfind  20954  lindsind  20955  mat1ghm  21086  mdetunilem1  21215  mdetunilem3  21217  mdetunilem4  21218  mdetunilem9  21223  cramerimplem2  21287  mat2pmatlin  21337  monmatcollpw  21381  cpmadugsumlemF  21478  mretopd  21694  neiptopnei  21734  neitr  21782  ufilen  22532  flimrest  22585  flimclslem  22586  fclsrest  22626  cnextcn  22669  haustsms2  22739  tsmsxplem2  22756  trust  22832  utoptop  22837  restutop  22840  ustuqtop4  22847  utopsnneiplem  22850  utop2nei  22853  utop3cls  22854  isucn2  22882  ucncn  22888  fmucnd  22895  trcfilu  22897  comet  23117  metustexhalf  23160  metustbl  23170  psmetutop  23171  nrmmetd  23178  reconnlem1  23428  reconnlem2  23429  fsumcn  23472  cmetcaulem  23885  iscmet3lem1  23888  iscmet3lem2  23889  bcthlem5  23925  cmslsschl  23974  rrxdstprj1  24006  minveclem4  24029  ovolfiniun  24096  itg1addlem4  24294  itg1addlem5  24295  itgsplitioo  24432  c1liplem1  24587  dvfsumlem1  24617  plyeq0lem  24794  quotcan  24892  psercnlem1  25007  cxplea  25273  birthdaylem3  25525  musumsum  25763  dvdsmulf1o  25765  dchrelbas4  25813  dchrhash  25841  gausslemma2dlem0d  25929  gausslemma2dlem1a  25935  2lgslem1a1  25959  2sqlem8a  25995  2sqlem8  25996  2sqcoprm  26005  2sqmod  26006  chto1ub  26046  vmadivsum  26052  dchrisumlem1  26059  dchrvmasumlem2  26068  dchrvmasumiflem1  26071  rpvmasum2  26082  mulog2sumlem2  26105  selberg2lem  26120  pntrmax  26134  pntpbnd1  26156  pntlemb  26167  pntlemj  26173  tgjustc1  26255  tgjustc2  26256  ercgrg  26297  motcgr  26316  tglineeltr  26411  colline  26429  miriso  26450  midexlem  26472  perpneq  26494  foot  26502  f1otrg  26651  axcontlem9  26752  uspgr1ewop  27024  nbupgrres  27140  structtocusgr  27222  wlkp1  27457  clwlkl1loop  27558  uspgrn2crct  27580  crctcshwlkn0lem5  27586  3trlond  27946  3pthond  27948  3spthond  27950  frgr3v  28048  vdgn1frgrv2  28069  numclwwlk3  28158  nmblolbii  28570  minvecolem3  28647  minvecolem4  28651  htthlem  28688  bcs2  28953  nmopub2tALT  29680  nmfnleub2  29697  eighmorth  29735  nmophmi  29802  nmopcoadji  29872  hstle  30001  atcvat3i  30167  opreu2reuALT  30234  disjxpin  30332  fmptco1f1o  30372  off2  30382  xppreima2  30389  fgreu  30411  suppovss  30420  1stpreimas  30435  padct  30449  resf1o  30460  fpwrelmap  30463  xrofsup  30486  eliccelico  30494  elicoelioo  30495  iocinif  30498  difioo  30499  prmdvdsbc  30526  ccatf1  30620  pfxlsw2ccat  30621  wrdt2ind  30622  ressprs  30637  tleile  30643  xrge0addgt0  30673  xrge0adddir  30674  omndmul3  30709  gsumle  30720  symgcom  30722  pmtrcnel  30728  pmtrcnel2  30729  pmtrcnelor  30730  cycpmfv2  30751  trsp2cyc  30760  cycpmco2lem7  30769  cyc3genpm  30789  cycpmconjslem2  30792  cyc3conja  30794  archirng  30812  archirngz  30813  orngmul  30871  linds2eq  30936  isprmidlc  30958  qsidomlem1  30960  qsidomlem2  30961  lindsunlem  31015  lbsdiflsp0  31017  fedgmullem1  31020  fedgmullem2  31021  1smat1  31064  madjusmdetlem2  31088  qtophaus  31095  locfinref  31100  metideq  31128  sqsscirc2  31147  tpr2rico  31150  fmcncfil  31169  lmxrge0  31190  lmdvg  31191  qqhval2lem  31217  qqhf  31222  qqhnm  31226  esumle  31312  gsumesum  31313  esumlef  31316  esumrnmpt2  31322  esumpcvgval  31332  esum2d  31347  ofcf  31357  ldsysgenld  31414  ldgenpisyslem1  31417  unelros  31425  difelros  31426  inelsros  31432  diffiunisros  31433  imambfm  31515  omssubadd  31553  inelcarsg  31564  carsgsigalem  31568  carsggect  31571  carsgclctunlem2  31572  oddpwdc  31607  eulerpartlems  31613  eulerpartlemb  31621  eulerpartlemt  31624  iwrdsplit  31640  sseqfn  31643  sseqf  31645  sseqfres  31646  ballotlemfc0  31745  ballotlemfcc  31746  ballotlemfrcn0  31782  sgnsub  31797  plymulx0  31812  signsplypnf  31815  signsvtn0  31835  signstfvneq0  31837  signsvtp  31848  signsvtn  31849  fsum2dsub  31873  reprlt  31885  hashreprin  31886  reprgt  31887  reprpmtf1o  31892  chtvalz  31895  breprexplema  31896  breprexplemc  31898  breprexp  31899  circlemeth  31906  logdivsqrle  31916  hgt750lemb  31922  lpadlem3  31944  lpadleft  31949  bnj927  32035  bnj1536  32121  bnj1001  32226  bnj1280  32287  cvxsconn  32485  satffunlem1  32649  satffunlem2  32650  elmrsubrn  32762  frpomin  33073  noextend  33168  neibastop3  33705  finxpsuclem  34672  poimirlem16  34902  poimirlem19  34905  poimirlem20  34906  poimirlem29  34915  mblfinlem3  34925  itg2addnclem3  34939  ftc1cnnclem  34959  lautlt  37221  lautcvr  37222  lauteq  37225  lautco  37227  ltrncl  37255  ltrncnvleN  37260  trljat2  37297  cdlemc6  37326  cdleme20c  37441  cdleme20j  37448  cdleme22e  37474  cdleme22eALTN  37475  cdlemg7aN  37755  cdlemg12e  37777  cdlemg17dALTN  37794  cdlemh  37947  cdlemkfid1N  38051  dibglbN  38296  diblss  38300  diclspsn  38324  dih1  38416  dihglbcpreN  38430  dihmeetlem4preN  38436  lcfrlem19  38691  mapfzcons  39306  mzpcl34  39321  mzpindd  39336  mzpsubst  39338  diophrw  39349  diophren  39403  irrapxlem1  39412  pellexlem5  39423  acongrep  39570  pwssplit4  39682  brtrclfv2  40065  rfovcnvf1od  40343  ntrk0kbimka  40382  isotone1  40391  isotone2  40392  4an4132  40826  mulltgt0  41272  fnchoice  41279  3adantlr3  41291  3adantll2  41293  3adantll3  41294  uzwo4  41308  disjf1o  41444  supxrgelem  41597  infleinflem2  41631  xrralrecnnle  41645  supxrunb3  41664  unb2ltle  41681  infrpgernmpt  41733  iooiinicc  41810  iooiinioc  41824  fmuldfeq  41856  mccl  41871  limccog  41893  limcrecl  41902  lptioo1  41905  islpcn  41912  limsupre  41914  neglimc  41920  0ellimcdiv  41922  limclner  41924  climleltrp  41949  climinf3  41989  liminflimsupclim  42080  xlimpnfxnegmnf  42087  icccncfext  42162  fprodcncf  42176  dvnmptdivc  42215  dvnmul  42220  dvmptfprod  42222  dvnprodlem3  42225  stoweidlem25  42303  stoweidlem34  42312  stoweidlem38  42316  stoweidlem44  42322  stoweidlem48  42326  stoweidlem49  42327  stoweidlem59  42337  stoweidlem60  42338  wallispilem4  42346  stirlinglem5  42356  dirkercncflem2  42382  fourierdlem39  42424  fourierdlem42  42427  fourierdlem46  42430  fourierdlem47  42431  fourierdlem48  42432  fourierdlem50  42434  fourierdlem51  42435  fourierdlem64  42448  fourierdlem73  42457  fourierdlem74  42458  fourierdlem77  42461  fourierdlem80  42464  fourierdlem87  42471  fourierdlem94  42478  fourierdlem103  42487  fourierdlem104  42488  etransclem32  42544  rrxsnicc  42578  sge0cl  42656  sge0f1o  42657  nnfoctbdjlem  42730  ismeannd  42742  omeiunltfirp  42794  hoicvr  42823  ovncvrrp  42839  hoidmvlelem2  42871  hoidmvlelem5  42874  hspdifhsp  42891  hoiqssbllem2  42898  hspmbllem2  42902  vonicclem2  42959  smflimsuplem7  43093  fundcmpsurbijinj  43563  sqrtpwpw2p  43693  isomgrref  43993  lincresunit2  44526  nnpw2pmod  44636  dignn0flhalflem1  44668  dignn0flhalf  44671  rrx2linest  44722  itsclc0yqsol  44744  itsclc0b  44752
  Copyright terms: Public domain W3C validator