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

Theorem syl12anc 856
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 . . 3 (𝜑𝜓)
2 syl12anc.2 . . 3 (𝜑𝜒)
3 syl12anc.3 . . 3 (𝜑𝜃)
41, 2, 3jca32 507 . 2 (𝜑 → (𝜓 ∧ (𝜒𝜃)))
5 syl12anc.4 . 2 ((𝜓 ∧ (𝜒𝜃)) → 𝜏)
64, 5syl 17 1 (𝜑𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 198  df-an 385
This theorem is referenced by:  syl22anc  858  raaan  4286  soltmin  5756  xpdifid  5786  f1dom3fv3dif  6758  f1prex  6772  cocan1  6779  fliftfun  6795  soisores  6810  soisoi  6811  isopolem  6828  f1oiso2  6835  weniso  6837  caovcld  7066  caovcomd  7069  onminex  7246  tfrlem12  7730  omeulem1  7908  oaabs2  7971  omabs  7973  erov  8089  findcard2d  8450  frfi  8453  finsschain  8521  suplub2  8615  supgtoreq  8624  supisolem  8627  ordiso2  8668  ordtypelem7  8677  wemaplem2  8700  wemapsolem  8703  cantnflt  8825  cantnfp1lem3  8833  cantnflem1b  8839  cantnflem1  8842  wemapwe  8850  cnfcomlem  8852  cnfcom  8853  cnfcom3lem  8856  infxpenlem  9128  fseqenlem1  9139  dfac12lem2  9260  infpssrlem4  9422  enfin2i  9437  isf34lem7  9495  isf34lem6  9496  fin1a2lem7  9522  fin1a2lem10  9525  fin1a2lem11  9526  fin1a2lem13  9528  ttukeylem6  9630  ttukeylem7  9631  iundom2g  9656  fpwwe2lem6  9751  fpwwe2lem7  9752  fpwwe2lem9  9754  fpwwe2lem12  9757  fpwwe2  9759  canthnumlem  9764  canthwelem  9766  canthp1lem2  9769  pwfseqlem4  9778  inar1  9891  intgru  9930  distrlem4pr  10142  conjmul  11036  lediv12a  11210  recp1lt1  11215  cju  11310  gtndiv  11739  zsupss  12015  uzsupss  12018  icc0  12460  iccssioo2  12483  ioounsnOLD  12539  fzrev3  12648  ico01fl0  12863  fldiv  12902  modabs  12946  modltm1p1mod  12965  modifeq2int  12975  seqcaopr  13080  seqf1olem1  13082  seqof2  13101  crreczi  13231  seqcoll  13484  seqcoll2  13485  hashtpg  13503  swrdccat3b  13739  sqrlem2  14226  resqrex  14233  abs1m  14317  isercoll  14640  zsum  14691  fsum2dlem  14743  fsumcom2  14747  fprod2dlem  14950  fprodcom2  14954  efsub  15069  bitsinv2  15403  sqgcd  15516  qredeu  15609  isprm7  15656  pcpremul  15784  pceulem  15786  pczpre  15788  pcdiv  15793  pcqmul  15794  pcqdiv  15798  pcexp  15800  pcdvdsb  15809  pcneg  15814  pcdvdstr  15816  pcgcd1  15817  pc2dvds  15819  pcz  15821  pcaddlem  15828  pcadd  15829  qexpz  15841  expnprm  15842  infpnlem2  15851  ramub2  15954  ramub1lem1  15966  setsstruct2  16126  f1ocpbllem  16408  f1ovscpbl  16410  mreexexlem3d  16530  mreexexlem4d  16531  fthi  16801  ipodrsima  17389  mndpropd  17540  grpsubpropd2  17745  ghmf1  17910  symgfvne  18028  f1omvdmvd  18083  f1otrspeq  18087  pmtrdifwrdel  18125  pmtrdifwrdel2  18126  psgnunilem2  18135  psgnunilem3  18136  psgnvalii  18149  odf1  18199  lsmpropd  18310  ablnnncan  18448  gsummptshft  18556  dprdf1o  18652  pgpfac1lem3  18697  pgpfac1lem5  18699  pgpfaclem1  18701  ablfaclem2  18706  srgbinomlem3  18763  ringpropd  18803  f1rhm0to0  18963  lmodprop2d  19148  lsspropd  19243  lmhmpropd  19299  lbspropd  19325  lbsextlem3  19388  assapropd  19555  psrass1  19633  psrass23l  19636  psrass23  19638  mplsubrg  19668  mplmon  19691  mplmonmul  19692  mplcoe1  19693  mplbas2  19698  mplind  19729  evlslem2  19739  mpfind  19763  gsumply1subr  19831  psrplusgpropd  19833  ply1scln0  19888  iporthcom  20209  obslbs  20304  scmataddcl  20553  scmatsubcl  20554  scmatmulcl  20555  smatvscl  20561  scmatrhmcl  20565  mat1scmat  20576  smadiadetglem2  20710  cramerimplem2  20723  cramerimplem3  20724  cramerimp  20725  1pmatscmul  20740  mat2pmatf1  20767  pm2mp  20863  chmatcl  20866  chmatval  20867  chmaidscmat  20886  chfacfisf  20892  cayhamlem1  20904  cpmidgsumm2pm  20907  cpmidpmat  20911  cpmadugsumfi  20915  cpmadumatpoly  20921  cayhamlem3  20925  pptbas  21046  elcls  21111  neiint  21142  neiptopnei  21170  restbas  21196  neitr  21218  iscnp4  21301  cnconst2  21321  cnpdis  21331  cnt0  21384  cnhaus  21392  cmpcovf  21428  hauscmplem  21443  conncompid  21468  2ndci  21485  2ndc1stc  21488  1stcrest  21490  2ndcctbss  21492  2ndcomap  21495  2ndcsep  21496  dis2ndc  21497  restlly  21520  islly2  21521  lly1stc  21533  dislly  21534  finlocfin  21557  dissnlocfin  21566  locfindis  21567  llycmpkgen2  21587  ptbasfi  21618  neitx  21644  ptpjopn  21649  ptcnplem  21658  upxp  21660  txlly  21673  txtube  21677  tx1stc  21687  txkgen  21689  xkococnlem  21696  kqreglem1  21778  kqreglem2  21779  kqnrmlem1  21780  kqnrmlem2  21781  hmeoimaf1o  21807  reghmph  21830  nrmhmph  21831  ordthmeolem  21838  trfil2  21924  fmfnfm  21995  hauspwpwf1  22024  fclsfnflim  22064  cnextf  22103  cnextcn  22104  tmdgsum2  22133  symgtgp  22138  subgntr  22143  opnsubg  22144  ghmcnp  22151  qustgpopn  22156  tsmsf1o  22181  tsmsxplem1  22189  tsmsxplem2  22190  tsmsxp  22191  ustexsym  22252  restutop  22274  imasdsf1olem  22411  blssexps  22464  blssex  22465  ssblex  22466  imasf1oxms  22527  blcld  22543  stdbdmopn  22556  met1stc  22559  met2ndci  22560  prdsxmslem2  22567  metcnp3  22578  cfilucfil  22597  ngptgp  22673  tgioo  22832  tgqioo  22836  zdis  22852  iccpnfhmeo  22977  xrhmeo  22978  cnheibor  22987  elpi1i  23078  cmetcusp  23383  pjthlem2  23443  ivthlem2  23455  ovolicc1  23519  ovolicc2lem3  23522  ovolicc2lem4  23523  volsup  23559  volivth  23610  vitalilem3  23613  mbflimsup  23669  mbfi1fseqlem1  23718  mbfi1fseqlem3  23720  mbfi1fseqlem5  23722  limcnlp  23878  limcflf  23881  limciun  23894  dvmptfsum  23974  dvcnvlem  23975  dvcvx  24019  facth1  24160  elply2  24188  plypf1  24204  coeeq  24219  aaliou3lem8  24336  ulm2  24375  mtestbdd  24395  reeff1o  24437  dcubic2  24807  quart  24824  xrlimcnp  24931  amgm  24953  harmonicbnd4  24973  perfect  25192  dchrptlem1  25225  bposlem2  25246  lgsfcl2  25264  lgsdir  25293  lgsdi  25295  lgsne0  25296  2lgslem1a1  25350  dchrvmasumlem2  25423  chpdifbndlem2  25479  pntpbnd1  25511  pntpbnd2  25512  padicabv  25555  tgcgrxfr  25649  idmot  25668  legid  25718  btwnleg  25719  leg0  25723  tghilberti1  25768  mirreu3  25785  colperpex  25861  lnopp2hpgb  25891  axcgrrflx  26030  axsegconlem1  26033  axcontlem2  26081  axcontlem12  26091  eengtrkg  26101  wwlksnredwwlkn  27054  clwwlkel  27217  clwlksfclwwlkOLD  27258  clwwlknonex2lem2  27299  0wlkon  27315  0trlon  27319  upgr3v3e3cycl  27375  frgrogt3nreg  27607  nvpi  27872  nmlno0lem  27998  fh1  28827  fh2  28828  nmlnop0iALT  29204  nmopun  29223  branmfn  29314  opsqrlem1  29349  opsqrlem6  29354  mdslmd1lem1  29534  csmdsymi  29543  atom1d  29562  chirredlem2  29600  cdj1i  29642  cdj3i  29650  fcnvgreu  29821  xrofsup  29882  2sqmod  29995  archirngz  30090  archiabllem2a  30095  gsummpt2d  30128  orngsqr  30151  ornglmullt  30154  orngrmullt  30155  metideq  30283  metider  30284  pstmfval  30286  lmxrge0  30345  qqhval2  30373  qqhf  30377  qqhghm  30379  qqhrhm  30380  esumpcvgval  30487  esum2dlem  30501  esum2d  30502  sigainb  30546  insiga  30547  ddemeas  30646  imambfm  30671  dya2icoseg  30686  dya2iocnrect  30690  eulerpartlemgvv  30785  probun  30828  ballotlemfc0  30901  ballotlemfcc  30902  sgnmul  30951  signstfvneq0  30996  breprexplemc  31057  erdszelem8  31524  erdszelem9  31525  erdsze2lem2  31530  cnpconn  31556  txpconn  31558  ptpconn  31559  indispconn  31560  connpconn  31561  cvxpconn  31568  cnllysconn  31571  cvmcov2  31601  cvmopnlem  31604  cvmliftmolem1  31607  cvmliftlem14  31623  cvmliftlem15  31624  cvmlift2lem13  31641  cvmlift3lem2  31646  cvmlift3lem9  31653  poseq  32095  sltres  32157  nolesgn2o  32166  nodense  32184  nosupbnd1lem3  32198  nosupbnd1lem5  32200  nosupbnd2lem1  32203  nocvxmin  32236  seglerflx  32561  seglemin  32562  btwnsegle  32566  hilbert1.1  32603  neibastop2lem  32697  bj-finsumval0  33482  relowlssretop  33545  wl-2sb6d  33673  tan2h  33732  poimirlem1  33741  poimirlem3  33743  poimirlem4  33744  poimirlem9  33749  poimirlem22  33762  poimirlem28  33768  heicant  33775  mblfinlem2  33778  itg2addnc  33794  ftc2nc  33824  dvasin  33826  sdclem1  33868  fdc  33870  istotbnd3  33899  sstotbnd  33903  prdstotbnd  33922  prdsbnd2  33923  cntotbnd  33924  rngoisocnv  34109  lsmsat  34806  islfld  34860  ps-2  35276  lplnexllnN  35362  4atlem9  35401  4atlem10a  35402  lnatexN  35577  2lnat  35582  pmapjat1  35651  lhpj1  35820  lhpm0atN  35827  4atexlemex2  35869  4atex  35874  4atex2-0aOLDN  35876  4atex2-0cOLDN  35878  lautcnvle  35887  lautj  35891  lautm  35892  idltrn  35948  cdleme01N  36019  cdleme0ex1N  36021  cdleme5  36038  cdleme9  36051  cdleme11c  36059  cdleme11g  36063  cdlemefrs29bpre0  36194  cdlemefrs29cpre1  36196  cdlemefrs32fva1  36199  cdleme32fva  36235  cdleme32fva1  36236  cdleme32fvaw  36237  cdleme32d  36242  cdleme32f  36244  cdleme35fnpq  36247  cdleme48d  36333  cdleme48gfv  36335  cdleme50ltrn  36355  trlord  36367  cdlemg4b1  36407  cdlemg4b2  36408  cdlemg13a  36449  cdlemg17a  36459  cdlemg17f  36464  erng1lem  36785  erngdvlem3  36788  erngdvlem4  36789  erng1r  36793  erngdvlem3-rN  36796  erngdvlem4-rN  36797  dva0g  36825  dialss  36844  dia0  36850  dia1N  36851  diaglbN  36853  diameetN  36854  diainN  36855  diaintclN  36856  dia1dim  36859  dia2dimlem5  36866  dia2dimlem7  36868  dia2dimlem9  36870  dia2dimlem10  36871  dia2dimlem12  36873  dia2dimlem13  36874  dvhopvadd  36891  dvhvaddass  36895  dvhopvsca  36900  tendolinv  36903  tendorinv  36904  dvhlveclem  36906  dvh0g  36909  dvheveccl  36910  dvhopN  36914  docaclN  36922  diaocN  36923  djajN  36935  dib0  36962  dib1dim  36963  dibglbN  36964  dibintclN  36965  dib1dim2  36966  diblss  36968  diblsmopel  36969  dicvaddcl  36988  dicvscacl  36989  diclspsn  36992  cdlemn4a  36997  cdlemn11c  37007  dihjustlem  37014  dihord1  37016  dihord2a  37017  dihord2b  37018  dihord2cN  37019  dihord11b  37020  dihord11c  37022  dihord2pre  37023  dihlsscpre  37032  dih1dimb  37038  dib2dim  37041  dih2dimb  37042  dih2dimbALTN  37043  dihvalcq2  37045  dihopelvalcpre  37046  dihord6apre  37054  dihord5b  37057  dihord5apre  37060  dih0  37078  dihmeetlem1N  37088  dihglblem5apreN  37089  dihglblem3N  37093  dihmeetlem2N  37097  dihglbcpreN  37098  dihmeetlem4preN  37104  dih1dimatlem0  37126  dih1dimatlem  37127  dihatlat  37132  dihatexv  37136  dihglb2  37140  dihmeet  37141  dihintcl  37142  dihmeet2  37144  doch2val2  37162  dochocss  37164  dihoml4c  37174  dochdmj1  37188  djhlj  37199  djhljjN  37200  djhjlj  37201  dihsumssj  37206  djhexmid  37209  djhlsmcl  37212  djhcvat42  37213  dihjatcclem4  37219  dihjat1lem  37226  dihsmsprn  37228  dihjat3  37230  dvh3dim2  37246  dvh3dim3N  37247  dochkr1OLDN  37277  lclkrlem2c  37307  lclkrlem2d  37308  mapdpglem23  37492  hdmap11lem2  37640  mzpcompact2lem  37833  diophrw  37841  rexrabdioph  37877  eldioph4b  37894  pellexlem5  37916  pellfund14  37981  acongtr  38063  fnwe2lem3  38140  gicabl  38187  hbtlem2  38212  hbtlem4  38214  hbtlem5  38216  dgraalem  38233  aaitgo  38250  ntrclsk13  38886  gneispb  38946  wessf1ornlem  39877  ltdiv23neg  40113  islptre  40348  limclner  40380  icccncfext  40597  stoweidlem1  40714  stoweidlem14  40727  stoweidlem24  40737  stoweidlem46  40759  stoweidlem57  40770  dirkercncflem2  40817  fourierdlem20  40840  fourierdlem41  40861  fourierdlem46  40865  fourierdlem48  40867  fourierdlem50  40869  fourierdlem62  40881  fourierdlem63  40882  fourierdlem64  40883  fourierdlem65  40884  fourierdlem76  40895  fourierdlem79  40898  fourierdlem103  40922  fourierdlem104  40923  etransclem47  40994  raaan2  41666  iccpartiun  41962  sqrtpwpw2p  42042  fmtnoprmfac1lem  42068  fmtnoprmfac2lem1  42070  lighneallem4a  42117  perfectALTV  42224  nnsum4primeseven  42280  nnsum4primesevenALTV  42281  mgmpropd  42360  lidlmmgm  42510  gsumlsscl  42749  lincsumcl  42805  lincscmcl  42806  isldepslvec2  42859  m1modmmod  42901  elbigo2  42931  relogbdivb  42941  blennnt2  42968  dignn0ldlem  42981
  Copyright terms: Public domain W3C validator