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

Theorem syl21anc 837
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 513 . 2 (𝜑 → (𝜓𝜒))
4 syl12anc.3 . 2 (𝜑𝜃)
5 syl21anc.4 . 2 (((𝜓𝜒) ∧ 𝜃) → 𝜏)
63, 4, 5syl2anc 585 1 (𝜑𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397
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 206  df-an 398
This theorem is referenced by:  syl1111anc  839  wereu2  5631  frpomin  6295  funtpg  6557  funcnvtp  6565  funcnvqp  6566  fnund  6616  fun2d  6707  fvun1  6933  iinpreima  7020  ftpg  7103  fsnunf  7132  f1prex  7231  soisores  7273  isotr  7282  off  7636  caofrss  7654  caonncan  7659  fvmpocurryd  8203  oaf1o  8511  omeulem1  8530  oeordi  8535  oelimcl  8548  oeeulem  8549  oeeui  8550  oaabs2  8596  omabs  8598  coflton  8618  pmresg  8809  ralxpmap  8835  domunsncan  9017  sucdom2OLD  9027  sucdom2  9151  unxpdom2  9199  sucxpdom  9200  unblem4  9243  fodomfi  9270  hartogslem1  9479  cantnflt  9609  cantnflem3  9628  cantnflem4  9629  cnfcomlem  9636  cnfcom  9637  ttrcltr  9653  infxpenlem  9950  infxpenc  9955  fseqenlem1  9961  pwsdompw  10141  cfeq0  10193  cofsmo  10206  cfsmolem  10207  ssfin4  10247  hsmexlem4  10366  hsmexlem5  10367  axdc3lem2  10388  fpwwe2  10580  wunpr  10646  mulclpi  10830  mulcanenq  10897  distrlem4pr  10963  prlem934  10970  prlem936  10984  divge0d  12998  elfznelfzob  13679  seqcaopr2  13945  facavg  14202  swrdwrdsymb  14551  cats1un  14610  f1oun2prg  14807  sqrtdiv  15151  sqrtdivd  15309  mulcn2  15479  o1of2  15496  fsumsplit  15627  sumsplit  15654  isumless  15731  demoivreALT  16084  rpnnen2lem11  16107  gcdnncl  16388  qredeu  16535  rpdvds  16537  isprm5  16584  rpexp  16599  divnumden  16624  divdenle  16625  phimullem  16652  phisum  16663  pythagtriplem4  16692  pythagtriplem8  16696  pythagtriplem9  16697  pcgcd1  16750  sumhash  16769  fldivp1  16770  pockthlem  16778  setsfun  17044  setsfun0  17045  ssc2  17706  estrreslem1  18025  estrreslem1OLD  18026  tleile  18311  mndpropd  18582  grpidssd  18824  grpinvssd  18825  issubg2  18944  isnsg3  18963  eqgid  18983  gass  19082  symgextres  19208  gsmsymgreqlem2  19214  sylow1lem5  19385  sylow2alem2  19401  sylow3lem3  19412  efgredlemd  19527  efgredlem  19530  frgpnabllem1  19652  frgpnabllem2  19653  subgdmdprd  19814  ablfacrplem  19845  rglcom4d  19943  kerf1ghm  20178  issrngd  20323  lmodprop2d  20387  lsspropd  20481  pwssplit1  20523  lspvadd  20560  znidomb  20971  znrrg  20975  lindfind  21225  lindsind  21226  mplsubglem  21408  mplind  21481  mat1ghm  21835  mdetunilem1  21964  mdetunilem3  21966  mdetunilem4  21967  mdetunilem9  21972  cramerimplem2  22036  mat2pmatlin  22087  monmatcollpw  22131  cpmadugsumlemF  22228  mretopd  22446  neiptopnei  22486  neitr  22534  ufilen  23284  flimrest  23337  flimclslem  23338  fclsrest  23378  cnextcn  23421  haustsms2  23491  tsmsxplem2  23508  trust  23584  utoptop  23589  restutop  23592  ustuqtop4  23599  utopsnneiplem  23602  utop2nei  23605  utop3cls  23606  isucn2  23634  ucncn  23640  fmucnd  23647  trcfilu  23649  comet  23872  metustexhalf  23915  metustbl  23925  psmetutop  23926  nrmmetd  23933  reconnlem1  24192  reconnlem2  24193  fsumcn  24236  cmetcaulem  24655  iscmet3lem1  24658  iscmet3lem2  24659  bcthlem5  24695  cmslsschl  24744  rrxdstprj1  24776  minveclem4  24799  ovolfiniun  24868  itg1addlem4  25066  itg1addlem4OLD  25067  itg1addlem5  25068  itgsplitioo  25205  c1liplem1  25363  dvfsumlem1  25393  plyeq0lem  25574  quotcan  25672  psercnlem1  25787  cxplea  26054  birthdaylem3  26306  musumsum  26544  dvdsmulf1o  26546  dchrelbas4  26594  dchrhash  26622  gausslemma2dlem0d  26710  gausslemma2dlem1a  26716  2lgslem1a1  26740  2sqlem8a  26776  2sqlem8  26777  2sqcoprm  26786  2sqmod  26787  chto1ub  26827  vmadivsum  26833  dchrisumlem1  26840  dchrvmasumlem2  26849  dchrvmasumiflem1  26852  rpvmasum2  26863  mulog2sumlem2  26886  selberg2lem  26901  pntrmax  26915  pntpbnd1  26937  pntlemb  26948  pntlemj  26954  noextend  27017  cuteq0  27174  tgjustc1  27420  tgjustc2  27421  ercgrg  27462  motcgr  27481  tglineeltr  27576  colline  27594  miriso  27615  midexlem  27637  perpneq  27659  foot  27667  f1otrg  27816  axcontlem9  27924  uspgr1ewop  28199  nbupgrres  28315  structtocusgr  28397  wlkp1  28632  clwlkl1loop  28734  uspgrn2crct  28756  crctcshwlkn0lem5  28762  3trlond  29120  3pthond  29122  3spthond  29124  frgr3v  29222  vdgn1frgrv2  29243  numclwwlk3  29332  nmblolbii  29744  minvecolem3  29821  minvecolem4  29825  htthlem  29862  bcs2  30127  nmopub2tALT  30854  nmfnleub2  30871  eighmorth  30909  nmophmi  30976  nmopcoadji  31046  hstle  31175  atcvat3i  31341  opreu2reuALT  31408  iinabrex  31490  disjxpin  31509  fmptco1f1o  31550  off2  31560  xppreima2  31570  fgreu  31591  suppovss  31601  1stpreimas  31622  padct  31639  resf1o  31650  fpwrelmap  31653  xrofsup  31675  eliccelico  31683  elicoelioo  31684  iocinif  31687  difioo  31688  prmdvdsbc  31715  ccatf1  31808  pfxlsw2ccat  31809  wrdt2ind  31810  ressprs  31826  xrge0addgt0  31885  xrge0adddir  31886  gsumhashmul  31901  omndmul3  31924  gsumle  31935  symgcom  31937  pmtrcnel  31943  pmtrcnel2  31944  pmtrcnelor  31945  cycpmfv2  31966  trsp2cyc  31975  cycpmco2lem7  31984  cyc3genpm  32004  cycpmconjslem2  32007  cyc3conja  32009  archirng  32027  archirngz  32028  orngmul  32101  linds2eq  32171  nsgqusf1olem3  32196  ghmquskerlem1  32198  ghmqusker  32201  rhmpreimaidl  32203  elrspunidl  32206  isprmidlc  32223  qsidomlem1  32228  qsidomlem2  32229  ressply1evl  32275  lindsunlem  32322  lbsdiflsp0  32324  fedgmullem1  32327  fedgmullem2  32328  ply1annprmidl  32376  1smat1  32388  madjusmdetlem2  32412  qtophaus  32420  locfinref  32425  zarclssn  32457  zar0ring  32462  zarmxt1  32464  rhmpreimacnlem  32468  rhmpreimacn  32469  metideq  32477  sqsscirc2  32493  tpr2rico  32496  fmcncfil  32515  lmxrge0  32536  lmdvg  32537  qqhval2lem  32565  qqhf  32570  qqhnm  32574  esumle  32660  gsumesum  32661  esumlef  32664  esumrnmpt2  32670  esumpcvgval  32680  esum2d  32695  ofcf  32705  ldsysgenld  32762  ldgenpisyslem1  32765  unelros  32773  difelros  32774  inelsros  32780  diffiunisros  32781  imambfm  32865  omssubadd  32903  inelcarsg  32914  carsgsigalem  32918  carsggect  32921  carsgclctunlem2  32922  oddpwdc  32957  eulerpartlems  32963  eulerpartlemb  32971  eulerpartlemt  32974  iwrdsplit  32990  sseqf  32995  sseqfres  32996  ballotlemfc0  33095  ballotlemfcc  33096  ballotlemfrcn0  33132  sgnsub  33147  plymulx0  33162  signsplypnf  33165  signsvtn0  33185  signstfvneq0  33187  signsvtp  33198  signsvtn  33199  fsum2dsub  33223  reprlt  33235  hashreprin  33236  reprgt  33237  reprpmtf1o  33242  chtvalz  33245  breprexplema  33246  breprexplemc  33248  breprexp  33249  circlemeth  33256  logdivsqrle  33266  hgt750lemb  33272  lpadlem3  33294  lpadleft  33299  bnj1536  33469  bnj1001  33574  bnj1280  33635  cvxsconn  33840  satffunlem1  34004  satffunlem2  34005  elmrsubrn  34117  neibastop3  34837  finxpsuclem  35871  poimirlem16  36097  poimirlem19  36100  poimirlem20  36101  poimirlem29  36110  mblfinlem3  36120  itg2addnclem3  36134  ftc1cnnclem  36152  lautlt  38557  lautcvr  38558  lauteq  38561  lautco  38563  ltrncl  38591  ltrncnvleN  38596  trljat2  38633  cdlemc6  38662  cdleme20c  38777  cdleme20j  38784  cdleme22e  38810  cdleme22eALTN  38811  cdlemg7aN  39091  cdlemg12e  39113  cdlemg17dALTN  39130  cdlemh  39283  cdlemkfid1N  39387  dibglbN  39632  diblss  39636  diclspsn  39660  dih1  39752  dihglbcpreN  39766  dihmeetlem4preN  39772  lcfrlem19  40027  aks4d1p8d1  40544  fsuppind  40768  mapfzcons  41042  mzpcl34  41057  mzpindd  41072  mzpsubst  41074  diophrw  41085  diophren  41139  irrapxlem1  41148  pellexlem5  41159  acongrep  41307  pwssplit4  41419  omlimcl2  41579  onexoegt  41581  oasubex  41624  omlim2  41636  nnoeomeqom  41649  nnawordexg  41664  succlg  41665  oacl2g  41667  omabs2  41668  omcl2  41669  ofoafg  41671  ofoaf  41672  ofoaass  41677  naddcnfass  41686  omssrncard  41819  brtrclfv2  42006  rfovcnvf1od  42283  ntrk0kbimka  42318  isotone1  42327  isotone2  42328  4an4132  42788  mulltgt0  43234  fnchoice  43241  3adantlr3  43252  3adantll2  43253  3adantll3  43254  uzwo4  43268  disjf1o  43417  supxrgelem  43578  infleinflem2  43612  xrralrecnnle  43624  supxrunb3  43641  unb2ltle  43657  infrpgernmpt  43707  iooiinicc  43787  iooiinioc  43801  fmuldfeq  43831  mccl  43846  limccog  43868  limcrecl  43877  lptioo1  43880  islpcn  43887  limsupre  43889  neglimc  43895  0ellimcdiv  43897  limclner  43899  climleltrp  43924  climinf3  43964  liminflimsupclim  44055  xlimpnfxnegmnf  44062  icccncfext  44135  fprodcncf  44148  dvnmptdivc  44186  dvnmul  44191  dvmptfprod  44193  dvnprodlem3  44196  stoweidlem25  44273  stoweidlem34  44282  stoweidlem38  44286  stoweidlem44  44292  stoweidlem48  44296  stoweidlem49  44297  stoweidlem59  44307  stoweidlem60  44308  wallispilem4  44316  stirlinglem5  44326  dirkercncflem2  44352  fourierdlem39  44394  fourierdlem42  44397  fourierdlem46  44400  fourierdlem47  44401  fourierdlem48  44402  fourierdlem50  44404  fourierdlem51  44405  fourierdlem64  44418  fourierdlem73  44427  fourierdlem74  44428  fourierdlem77  44431  fourierdlem80  44434  fourierdlem87  44441  fourierdlem94  44448  fourierdlem103  44457  fourierdlem104  44458  etransclem32  44514  rrxsnicc  44548  sge0cl  44629  sge0f1o  44630  nnfoctbdjlem  44703  ismeannd  44715  omeiunltfirp  44767  hoicvr  44796  ovncvrrp  44812  hoidmvlelem2  44844  hoidmvlelem5  44847  hspdifhsp  44864  hoiqssbllem2  44871  hspmbllem2  44875  vonicclem2  44932  smflimsuplem7  45074  fundcmpsurbijinj  45609  sqrtpwpw2p  45737  isomgrref  46034  lincresunit2  46566  nnpw2pmod  46676  dignn0flhalflem1  46708  dignn0flhalf  46711  rrx2linest  46835  itsclc0yqsol  46857  itsclc0b  46865  functhinclem1  47068  functhinclem2  47069  fullthinc2  47074
  Copyright terms: Public domain W3C validator