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

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

Proof of Theorem syl12anc
StepHypRef Expression
1 syl12anc.1 . 2 (𝜑𝜓)
2 syl12anc.2 . . 3 (𝜑𝜒)
3 syl12anc.3 . . 3 (𝜑𝜃)
42, 3jca 512 . 2 (𝜑 → (𝜒𝜃))
5 syl12anc.4 . 2 ((𝜓 ∧ (𝜒𝜃)) → 𝜏)
61, 4, 5syl2anc 584 1 (𝜑𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  syl22anc  836  raaan  4462  raaanv  4463  raaan2  4466  soltmin  5993  xpdifid  6022  reuop  6141  f1dom3fv3dif  7023  f1prex  7037  cocan1  7044  fliftfun  7060  soisores  7075  soisoi  7076  isopolem  7093  f1oiso2  7100  weniso  7102  caovcld  7334  caovcomd  7337  onminex  7513  tfrlem12  8019  omeulem1  8201  oaabs2  8265  omabs  8267  erov  8387  findcard2d  8752  frfi  8755  finsschain  8823  suplub2  8917  supgtoreq  8926  supisolem  8929  ordiso2  8971  ordtypelem7  8980  wemaplem2  9003  wemapsolem  9006  cantnflt  9127  cantnfp1lem3  9135  cantnflem1b  9141  cantnflem1  9144  wemapwe  9152  cnfcomlem  9154  cnfcom  9155  cnfcom3lem  9158  infxpenlem  9431  fseqenlem1  9442  dfac12lem2  9562  infpssrlem4  9720  enfin2i  9735  isf34lem7  9793  isf34lem6  9794  fin1a2lem7  9820  fin1a2lem10  9823  fin1a2lem11  9824  fin1a2lem13  9826  ttukeylem6  9928  ttukeylem7  9929  iundom2g  9954  fpwwe2lem6  10049  fpwwe2lem7  10050  fpwwe2lem9  10052  fpwwe2lem12  10055  fpwwe2  10057  canthnumlem  10062  canthwelem  10064  canthp1lem2  10067  pwfseqlem4  10076  inar1  10189  intgru  10228  distrlem4pr  10440  conjmul  11349  lediv12a  11525  recp1lt1  11530  cju  11626  gtndiv  12051  zsupss  12329  uzsupss  12332  icc0  12779  iccssioo2  12802  fzrev3  12966  ico01fl0  13182  fldiv  13221  modabs  13265  modltm1p1mod  13284  modifeq2int  13294  modsumfzodifsn  13305  seqcaopr  13400  seqf1olem1  13402  seqof2  13421  crreczi  13582  seqcoll  13815  seqcoll2  13816  hashtpg  13836  swrdccat3b  14095  sqrlem2  14596  resqrex  14603  abs1m  14688  isercoll  15017  zsum  15068  fsum2dlem  15118  fsumcom2  15122  fprod2dlem  15327  fprodcom2  15331  efsub  15446  bitsinv2  15785  sqgcd  15902  qredeu  15995  isprm7  16045  pcpremul  16173  pceulem  16175  pczpre  16177  pcdiv  16182  pcqmul  16183  pcqdiv  16187  pcexp  16189  pcdvdsb  16198  pcneg  16203  pcdvdstr  16205  pcgcd1  16206  pc2dvds  16208  pcz  16210  pcaddlem  16217  pcadd  16218  qexpz  16230  expnprm  16231  infpnlem2  16240  ramub2  16343  ramub1lem1  16355  setsstruct2  16514  f1ocpbllem  16790  f1ovscpbl  16792  mreexexlem3d  16910  mreexexlem4d  16911  fthi  17181  ipodrsima  17768  mndpropd  17927  grpsubpropd2  18138  ghmf1  18320  symgfvne  18439  f1omvdmvd  18494  f1otrspeq  18498  pmtrdifwrdel  18536  pmtrdifwrdel2  18537  psgnunilem2  18546  psgnunilem3  18547  psgnvalii  18560  odf1  18612  lsmpropd  18726  ablnnncan  18866  gsummptshft  18979  dprdf1o  19077  pgpfac1lem3  19122  pgpfac1lem5  19124  pgpfaclem1  19126  ablfaclem2  19131  srgbinomlem3  19215  ringpropd  19255  f1ghm0to0  19415  f1rhm0to0OLD  19416  lmodprop2d  19619  lsspropd  19712  lmhmpropd  19768  lbspropd  19794  lbsextlem3  19855  assapropd  20023  psrass1  20107  psrass23l  20110  psrass23  20112  mplsubrg  20142  mplmon  20165  mplmonmul  20166  mplcoe1  20167  mplbas2  20172  mplind  20203  evlslem2  20213  mpfind  20240  gsumply1subr  20322  psrplusgpropd  20324  ply1scln0  20379  iporthcom  20698  obslbs  20793  scmataddcl  21044  scmatsubcl  21045  scmatmulcl  21046  smatvscl  21052  scmatrhmcl  21056  mat1scmat  21067  smadiadetglem2  21200  cramerimplem2  21212  cramerimplem3  21213  cramerimp  21214  1pmatscmul  21229  mat2pmatf1  21256  pm2mp  21352  chmatcl  21355  chmatval  21356  chmaidscmat  21375  chfacfisf  21381  cayhamlem1  21393  cpmidgsumm2pm  21396  cpmidpmat  21400  cpmadugsumfi  21404  cpmadumatpoly  21410  cayhamlem3  21414  pptbas  21535  elcls  21600  neiint  21631  neiptopnei  21659  restbas  21685  neitr  21707  iscnp4  21790  cnconst2  21810  cnpdis  21820  cnt0  21873  cnhaus  21881  cmpcovf  21918  hauscmplem  21933  conncompid  21958  2ndci  21975  2ndc1stc  21978  1stcrest  21980  2ndcctbss  21982  2ndcomap  21985  2ndcsep  21986  dis2ndc  21987  restlly  22010  islly2  22011  lly1stc  22023  dislly  22024  finlocfin  22047  dissnlocfin  22056  locfindis  22057  llycmpkgen2  22077  ptbasfi  22108  neitx  22134  ptpjopn  22139  ptcnplem  22148  upxp  22150  txlly  22163  txtube  22167  tx1stc  22177  txkgen  22179  xkococnlem  22186  kqreglem1  22268  kqreglem2  22269  kqnrmlem1  22270  kqnrmlem2  22271  hmeoimaf1o  22297  reghmph  22320  nrmhmph  22321  ordthmeolem  22328  trfil2  22414  fmfnfm  22485  hauspwpwf1  22514  fclsfnflim  22554  cnextf  22593  cnextcn  22594  tmdgsum2  22623  symgtgp  22628  subgntr  22633  opnsubg  22634  ghmcnp  22641  qustgpopn  22646  tsmsf1o  22671  tsmsxplem1  22679  tsmsxplem2  22680  tsmsxp  22681  ustexsym  22742  restutop  22764  imasdsf1olem  22901  blssexps  22954  blssex  22955  ssblex  22956  imasf1oxms  23017  blcld  23033  stdbdmopn  23046  met1stc  23049  met2ndci  23050  prdsxmslem2  23057  metcnp3  23068  cfilucfil  23087  ngptgp  23163  tgioo  23322  tgqioo  23326  zdis  23342  iccpnfhmeo  23467  xrhmeo  23468  cnheibor  23477  elpi1i  23568  cmetcusp  23875  bncssbn  23895  pjthlem2  23959  ivthlem2  23971  ovolicc1  24035  ovolicc2lem3  24038  ovolicc2lem4  24039  volsup  24075  volivth  24126  vitalilem3  24129  mbflimsup  24185  mbfi1fseqlem1  24234  mbfi1fseqlem3  24236  mbfi1fseqlem5  24238  limcnlp  24394  limcflf  24397  limciun  24410  dvmptfsum  24490  dvcnvlem  24491  dvcvx  24535  facth1  24676  elply2  24704  plypf1  24720  coeeq  24735  aaliou3lem8  24852  ulm2  24891  mtestbdd  24911  reeff1o  24953  logbgcd1irr  25288  dcubic2  25338  quart  25355  xrlimcnp  25463  amgm  25485  harmonicbnd4  25505  perfect  25724  dchrptlem1  25757  bposlem2  25778  lgsfcl2  25796  lgsdir  25825  lgsdi  25827  lgsne0  25828  2lgslem1a1  25882  2sqmod  25929  dchrvmasumlem2  25991  chpdifbndlem2  26047  pntpbnd1  26079  pntpbnd2  26080  padicabv  26123  tgcgrxfr  26221  idmot  26240  legid  26290  btwnleg  26291  leg0  26295  tghilberti1  26340  mirreu3  26357  colperpex  26436  lnopp2hpgb  26466  axcgrrflx  26617  axsegconlem1  26620  axcontlem2  26668  axcontlem12  26678  eengtrkg  26689  wwlksnredwwlkn  27590  0wlkon  27816  0trlon  27820  upgr3v3e3cycl  27876  frgrogt3nreg  28093  nvpi  28361  nmlno0lem  28487  fh1  29312  fh2  29313  nmlnop0iALT  29689  nmopun  29708  branmfn  29799  opsqrlem1  29834  opsqrlem6  29839  mdslmd1lem1  30019  csmdsymi  30028  atom1d  30047  chirredlem2  30085  cdj1i  30127  cdj3i  30135  fcnvgreu  30336  suppovss  30344  xrofsup  30408  gsummpt2d  30604  odpmco  30647  cycpmco2lem6  30690  cycpmco2  30692  cyc3evpm  30709  cycpmconjslem2  30714  archirngz  30735  archiabllem2a  30740  orngsqr  30794  ornglmullt  30797  orngrmullt  30798  lindssn  30856  lindfpropd  30859  lindsun  30910  dimkerim  30912  fedgmullem2  30915  metideq  31022  metider  31023  pstmfval  31025  lmxrge0  31084  qqhval2  31112  qqhf  31116  qqhghm  31118  qqhrhm  31119  esumpcvgval  31226  esum2dlem  31240  esum2d  31241  sigainb  31284  insiga  31285  ddemeas  31384  imambfm  31409  dya2icoseg  31424  dya2iocnrect  31428  eulerpartlemgvv  31523  probun  31566  ballotlemfc0  31639  ballotlemfcc  31640  sgnmul  31689  breprexplemc  31792  erdszelem8  32332  erdszelem9  32333  erdsze2lem2  32338  cnpconn  32364  txpconn  32366  ptpconn  32367  indispconn  32368  connpconn  32369  cvxpconn  32376  cnllysconn  32379  cvmcov2  32409  cvmopnlem  32412  cvmliftmolem1  32415  cvmliftlem14  32431  cvmliftlem15  32432  cvmlift2lem13  32449  cvmlift3lem2  32454  cvmlift3lem9  32461  poseq  32982  sltres  33056  nolesgn2o  33065  nodense  33083  nosupbnd1lem3  33097  nosupbnd1lem5  33099  nosupbnd2lem1  33102  nocvxmin  33135  seglerflx  33460  seglemin  33461  btwnsegle  33465  hilbert1.1  33502  neibastop2lem  33595  bj-finsumval0  34445  relowlssretop  34516  wl-2sb6d  34664  tan2h  34754  poimirlem1  34763  poimirlem3  34765  poimirlem4  34766  poimirlem9  34771  poimirlem22  34784  poimirlem28  34790  heicant  34797  mblfinlem2  34800  itg2addnc  34816  ftc2nc  34846  dvasin  34848  sdclem1  34889  fdc  34891  istotbnd3  34920  sstotbnd  34924  prdstotbnd  34943  prdsbnd2  34944  cntotbnd  34945  rngoisocnv  35130  lsmsat  36014  islfld  36068  ps-2  36484  lplnexllnN  36570  4atlem9  36609  4atlem10a  36610  lnatexN  36785  2lnat  36790  pmapjat1  36859  lhpj1  37028  lhpm0atN  37035  4atexlemex2  37077  4atex  37082  4atex2-0aOLDN  37084  4atex2-0cOLDN  37086  lautcnvle  37095  lautj  37099  lautm  37100  idltrn  37156  cdleme01N  37227  cdleme0ex1N  37229  cdleme5  37246  cdleme9  37259  cdleme11c  37267  cdleme11g  37271  cdlemefrs29bpre0  37402  cdlemefrs29cpre1  37404  cdlemefrs32fva1  37407  cdleme32fva  37443  cdleme32fva1  37444  cdleme32fvaw  37445  cdleme32d  37450  cdleme32f  37452  cdleme35fnpq  37455  cdleme48d  37541  cdleme48gfv  37543  cdleme50ltrn  37563  trlord  37575  cdlemg4b1  37615  cdlemg4b2  37616  cdlemg13a  37657  cdlemg17a  37667  cdlemg17f  37672  erng1lem  37993  erngdvlem3  37996  erngdvlem4  37997  erng1r  38001  erngdvlem3-rN  38004  erngdvlem4-rN  38005  dva0g  38033  dialss  38052  dia0  38058  dia1N  38059  diaglbN  38061  diameetN  38062  diainN  38063  diaintclN  38064  dia1dim  38067  dia2dimlem5  38074  dia2dimlem7  38076  dia2dimlem9  38078  dia2dimlem10  38079  dia2dimlem12  38081  dia2dimlem13  38082  dvhopvadd  38099  dvhvaddass  38103  dvhopvsca  38108  tendolinv  38111  tendorinv  38112  dvhlveclem  38114  dvh0g  38117  dvheveccl  38118  dvhopN  38122  docaclN  38130  diaocN  38131  djajN  38143  dib0  38170  dib1dim  38171  dibglbN  38172  dibintclN  38173  dib1dim2  38174  diblss  38176  diblsmopel  38177  dicvaddcl  38196  dicvscacl  38197  diclspsn  38200  cdlemn4a  38205  cdlemn11c  38215  dihjustlem  38222  dihord1  38224  dihord2a  38225  dihord2b  38226  dihord2cN  38227  dihord11b  38228  dihord11c  38230  dihord2pre  38231  dihlsscpre  38240  dih1dimb  38246  dib2dim  38249  dih2dimb  38250  dih2dimbALTN  38251  dihvalcq2  38253  dihopelvalcpre  38254  dihord6apre  38262  dihord5b  38265  dihord5apre  38268  dih0  38286  dihmeetlem1N  38296  dihglblem5apreN  38297  dihglblem3N  38301  dihmeetlem2N  38305  dihglbcpreN  38306  dihmeetlem4preN  38312  dih1dimatlem0  38334  dih1dimatlem  38335  dihatlat  38340  dihatexv  38344  dihglb2  38348  dihmeet  38349  dihintcl  38350  dihmeet2  38352  doch2val2  38370  dochocss  38372  dihoml4c  38382  dochdmj1  38396  djhlj  38407  djhljjN  38408  djhjlj  38409  dihsumssj  38414  djhexmid  38417  djhlsmcl  38420  djhcvat42  38421  dihjatcclem4  38427  dihjat1lem  38434  dihsmsprn  38436  dihjat3  38438  dvh3dim2  38454  dvh3dim3N  38455  dochkr1OLDN  38485  lclkrlem2c  38515  lclkrlem2d  38516  mapdpglem23  38700  hdmap11lem2  38848  expgcd  39051  0prjspn  39138  mzpcompact2lem  39216  diophrw  39224  rexrabdioph  39259  eldioph4b  39276  pellexlem5  39298  pellfund14  39363  acongtr  39443  fnwe2lem3  39520  gicabl  39567  hbtlem2  39592  hbtlem4  39594  hbtlem5  39596  dgraalem  39613  aaitgo  39630  ntrclsk13  40289  gneispb  40349  wessf1ornlem  41313  ltdiv23neg  41534  islptre  41768  limclner  41800  icccncfext  42038  stoweidlem1  42155  stoweidlem14  42168  stoweidlem24  42178  stoweidlem46  42200  stoweidlem57  42211  dirkercncflem2  42258  fourierdlem20  42281  fourierdlem41  42302  fourierdlem46  42306  fourierdlem48  42308  fourierdlem50  42310  fourierdlem62  42322  fourierdlem63  42323  fourierdlem64  42324  fourierdlem65  42325  fourierdlem76  42336  fourierdlem79  42339  fourierdlem103  42363  fourierdlem104  42364  etransclem47  42435  iccpartiun  43429  reupr  43519  sqrtpwpw2p  43535  fmtnoprmfac1lem  43561  fmtnoprmfac2lem1  43563  lighneallem4a  43608  requad2  43623  perfectALTV  43723  nnsum4primeseven  43800  nnsum4primesevenALTV  43801  mgmpropd  43877  lidlmmgm  44031  gsumlsscl  44266  lincsumcl  44321  lincscmcl  44322  isldepslvec2  44375  m1modmmod  44416  elbigo2  44447  relogbdivb  44457  blennnt2  44484  dignn0ldlem  44497  itsclc0yqsollem2  44585  inlinecirc02p  44609
  Copyright terms: Public domain W3C validator