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

Theorem syl12anc 1364
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 557 . 2 (𝜑 → (𝜓 ∧ (𝜒𝜃)))
5 syl12anc.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:  syl22anc  1367  raaan  4115  soltmin  5567  xpdifid  5597  f1dom3fv3dif  6565  f1prex  6579  cocan1  6586  fliftfun  6602  soisores  6617  soisoi  6618  isopolem  6635  f1oiso2  6642  weniso  6644  caovcld  6869  caovcomd  6872  onminex  7049  tfrlem12  7530  omeulem1  7707  oaabs2  7770  omabs  7772  erov  7887  findcard2d  8243  frfi  8246  finsschain  8314  suplub2  8408  supgtoreq  8417  supisolem  8420  ordiso2  8461  ordtypelem7  8470  wemaplem2  8493  wemapsolem  8496  cantnflt  8607  cantnfp1lem3  8615  cantnflem1b  8621  cantnflem1  8624  wemapwe  8632  cnfcomlem  8634  cnfcom  8635  cnfcom3lem  8638  infxpenlem  8874  fseqenlem1  8885  dfac12lem2  9004  infpssrlem4  9166  enfin2i  9181  isf34lem7  9239  isf34lem6  9240  fin1a2lem7  9266  fin1a2lem10  9269  fin1a2lem11  9270  fin1a2lem13  9272  ttukeylem6  9374  ttukeylem7  9375  iundom2g  9400  fpwwe2lem6  9495  fpwwe2lem7  9496  fpwwe2lem9  9498  fpwwe2lem12  9501  fpwwe2  9503  canthnumlem  9508  canthwelem  9510  canthp1lem2  9513  pwfseqlem4  9522  inar1  9635  intgru  9674  distrlem4pr  9886  conjmul  10780  lediv12a  10954  recp1lt1  10959  cju  11054  gtndiv  11492  zsupss  11815  uzsupss  11818  icc0  12261  iccssioo2  12284  fzrev3  12444  ico01fl0  12660  fldiv  12699  modabs  12743  modltm1p1mod  12762  modifeq2int  12772  seqcaopr  12878  seqf1olem1  12880  seqof2  12899  crreczi  13029  seqcoll  13286  seqcoll2  13287  hashtpg  13305  swrdccat3b  13542  sqrlem2  14028  resqrex  14035  abs1m  14119  isercoll  14442  zsum  14493  fsum2dlem  14545  fsumcom2  14549  fsumcom2OLD  14550  fprod2dlem  14754  fprodcom2  14758  fprodcom2OLD  14759  efsub  14874  bitsinv2  15212  sqgcd  15325  qredeu  15419  isprm7  15467  pcpremul  15595  pceulem  15597  pczpre  15599  pcdiv  15604  pcqmul  15605  pcqdiv  15609  pcexp  15611  pcdvdsb  15620  pcneg  15625  pcdvdstr  15627  pcgcd1  15628  pc2dvds  15630  pcz  15632  pcaddlem  15639  pcadd  15640  qexpz  15652  expnprm  15653  infpnlem2  15662  ramub2  15765  ramub1lem1  15777  setsstruct2  15943  f1ocpbllem  16231  f1ovscpbl  16233  mreexexlem3d  16353  mreexexlem4d  16354  fthi  16625  ipodrsima  17212  mndpropd  17363  grpsubpropd2  17568  ghmf1  17736  symgfvne  17854  f1omvdmvd  17909  f1otrspeq  17913  pmtrdifwrdel  17951  pmtrdifwrdel2  17952  psgnunilem2  17961  psgnunilem3  17962  psgnvalii  17975  odf1  18025  lsmpropd  18136  ablnnncan  18274  gsummptshft  18382  dprdf1o  18477  pgpfac1lem3  18522  pgpfac1lem5  18524  pgpfaclem1  18526  ablfaclem2  18531  srgbinomlem3  18588  ringpropd  18628  f1rhm0to0  18788  lmodprop2d  18973  lsspropd  19065  lmhmpropd  19121  lbspropd  19147  lbsextlem3  19208  assapropd  19375  psrass1  19453  psrass23l  19456  psrass23  19458  mplsubrg  19488  mplmon  19511  mplmonmul  19512  mplcoe1  19513  mplbas2  19518  mplind  19550  evlslem2  19560  mpfind  19584  gsumply1subr  19652  psrplusgpropd  19654  ply1scln0  19709  iporthcom  20028  obslbs  20122  scmataddcl  20370  scmatsubcl  20371  scmatmulcl  20372  smatvscl  20378  scmatrhmcl  20382  mat1scmat  20393  smadiadetglem2  20526  cramerimplem2  20538  cramerimplem3  20539  cramerimp  20540  1pmatscmul  20555  mat2pmatf1  20582  pm2mp  20678  chmatcl  20681  chmatval  20682  chmaidscmat  20701  chfacfisf  20707  cayhamlem1  20719  cpmidgsumm2pm  20722  cpmidpmat  20726  cpmadugsumfi  20730  cpmadumatpoly  20736  cayhamlem3  20740  pptbas  20860  elcls  20925  neiint  20956  neiptopnei  20984  restbas  21010  neitr  21032  iscnp4  21115  cnconst2  21135  cnpdis  21145  cnt0  21198  cnhaus  21206  cmpcovf  21242  hauscmplem  21257  conncompid  21282  2ndci  21299  2ndc1stc  21302  1stcrest  21304  2ndcctbss  21306  2ndcomap  21309  2ndcsep  21310  dis2ndc  21311  restlly  21334  islly2  21335  lly1stc  21347  dislly  21348  finlocfin  21371  dissnlocfin  21380  locfindis  21381  llycmpkgen2  21401  ptbasfi  21432  neitx  21458  ptpjopn  21463  ptcnplem  21472  upxp  21474  txlly  21487  txtube  21491  tx1stc  21501  txkgen  21503  xkococnlem  21510  kqreglem1  21592  kqreglem2  21593  kqnrmlem1  21594  kqnrmlem2  21595  hmeoimaf1o  21621  reghmph  21644  nrmhmph  21645  ordthmeolem  21652  trfil2  21738  fmfnfm  21809  hauspwpwf1  21838  fclsfnflim  21878  cnextf  21917  cnextcn  21918  tmdgsum2  21947  symgtgp  21952  subgntr  21957  opnsubg  21958  ghmcnp  21965  qustgpopn  21970  tsmsf1o  21995  tsmsxplem1  22003  tsmsxplem2  22004  tsmsxp  22005  ustexsym  22066  restutop  22088  imasdsf1olem  22225  blssexps  22278  blssex  22279  ssblex  22280  imasf1oxms  22341  blcld  22357  stdbdmopn  22370  met1stc  22373  met2ndci  22374  prdsxmslem2  22381  metcnp3  22392  cfilucfil  22411  ngptgp  22487  tgioo  22646  tgqioo  22650  zdis  22666  iccpnfhmeo  22791  xrhmeo  22792  cnheibor  22801  elpi1i  22892  cmetcusp  23196  pjthlem2  23255  ivthlem2  23267  ovolicc1  23330  ovolicc2lem3  23333  ovolicc2lem4  23334  volsup  23370  volivth  23421  vitalilem3  23424  mbflimsup  23478  mbfi1fseqlem1  23527  mbfi1fseqlem3  23529  mbfi1fseqlem5  23531  limcnlp  23687  limcflf  23690  limciun  23703  dvmptfsum  23783  dvcnvlem  23784  dvcvx  23828  facth1  23969  elply2  23997  plypf1  24013  coeeq  24028  aaliou3lem8  24145  ulm2  24184  mtestbdd  24204  reeff1o  24246  dcubic2  24616  quart  24633  xrlimcnp  24740  amgm  24762  harmonicbnd4  24782  perfect  25001  dchrptlem1  25034  bposlem2  25055  lgsfcl2  25073  lgsdir  25102  lgsdi  25104  lgsne0  25105  2lgslem1a1  25159  dchrvmasumlem2  25232  chpdifbndlem2  25288  pntpbnd1  25320  pntpbnd2  25321  padicabv  25364  tgcgrxfr  25458  idmot  25477  legid  25527  btwnleg  25528  leg0  25532  tghilberti1  25577  mirreu3  25594  colperpex  25670  lnopp2hpgb  25700  axcgrrflx  25839  axsegconlem1  25842  axcontlem2  25890  axcontlem12  25900  eengtrkg  25910  wwlksnredwwlkn  26858  clwwlkel  27009  clwlksfclwwlk  27049  clwwlknonex2lem2  27083  0wlkon  27098  0trlon  27102  upgr3v3e3cycl  27158  frgrogt3nreg  27384  nvpi  27650  nmlno0lem  27776  fh1  28605  fh2  28606  eigposi  28823  nmlnop0iALT  28982  nmopun  29001  branmfn  29092  opsqrlem1  29127  opsqrlem6  29132  mdslmd1lem1  29312  csmdsymi  29321  atom1d  29340  chirredlem2  29378  cdj1i  29420  cdj3i  29428  fcnvgreu  29600  xrofsup  29661  2sqmod  29776  archirngz  29871  archiabllem2a  29876  gsummpt2d  29909  orngsqr  29932  ornglmullt  29935  orngrmullt  29936  metideq  30064  metider  30065  pstmfval  30067  lmxrge0  30126  qqhval2  30154  qqhf  30158  qqhghm  30160  qqhrhm  30161  esumpcvgval  30268  esum2dlem  30282  esum2d  30283  sigainb  30327  insiga  30328  ddemeas  30427  imambfm  30452  dya2icoseg  30467  dya2iocnrect  30471  eulerpartlemgvv  30566  probun  30609  ballotlemfc0  30682  ballotlemfcc  30683  sgnmul  30732  signstfvneq0  30777  breprexplemc  30838  erdszelem8  31306  erdszelem9  31307  erdsze2lem2  31312  cnpconn  31338  txpconn  31340  ptpconn  31341  indispconn  31342  connpconn  31343  cvxpconn  31350  cnllysconn  31353  cvmcov2  31383  cvmopnlem  31386  cvmliftmolem1  31389  cvmliftlem14  31405  cvmliftlem15  31406  cvmlift2lem13  31423  cvmlift3lem2  31428  cvmlift3lem9  31435  poseq  31878  sltres  31940  nolesgn2o  31949  nodense  31967  nosupbnd1lem3  31981  nosupbnd1lem5  31983  nosupbnd2lem1  31986  nocvxmin  32019  seglerflx  32344  seglemin  32345  btwnsegle  32349  hilbert1.1  32386  neibastop2lem  32480  bj-finsumval0  33277  relowlssretop  33341  wl-2sb6d  33471  tan2h  33531  poimirlem1  33540  poimirlem3  33542  poimirlem4  33543  poimirlem9  33548  poimirlem22  33561  poimirlem28  33567  heicant  33574  mblfinlem2  33577  itg2addnc  33594  ftc2nc  33624  dvasin  33626  sdclem1  33669  fdc  33671  istotbnd3  33700  sstotbnd  33704  prdstotbnd  33723  prdsbnd2  33724  cntotbnd  33725  rngoisocnv  33910  lsmsat  34613  islfld  34667  ps-2  35082  lplnexllnN  35168  4atlem9  35207  4atlem10a  35208  lnatexN  35383  2lnat  35388  pmapjat1  35457  lhpj1  35626  lhpm0atN  35633  4atexlemex2  35675  4atex  35680  4atex2-0aOLDN  35682  4atex2-0cOLDN  35684  lautcnvle  35693  lautj  35697  lautm  35698  idltrn  35754  cdleme01N  35826  cdleme0ex1N  35828  cdleme5  35845  cdleme9  35858  cdleme11c  35866  cdleme11g  35870  cdlemefrs29bpre0  36001  cdlemefrs29cpre1  36003  cdlemefrs32fva1  36006  cdleme32fva  36042  cdleme32fva1  36043  cdleme32fvaw  36044  cdleme32d  36049  cdleme32f  36051  cdleme35fnpq  36054  cdleme48d  36140  cdleme48gfv  36142  cdleme50ltrn  36162  trlord  36174  cdlemg4b1  36214  cdlemg4b2  36215  cdlemg13a  36256  cdlemg17a  36266  cdlemg17f  36271  erng1lem  36592  erngdvlem3  36595  erngdvlem4  36596  erng1r  36600  erngdvlem3-rN  36603  erngdvlem4-rN  36604  dva0g  36633  dialss  36652  dia0  36658  dia1N  36659  diaglbN  36661  diameetN  36662  diainN  36663  diaintclN  36664  dia1dim  36667  dia2dimlem5  36674  dia2dimlem7  36676  dia2dimlem9  36678  dia2dimlem10  36679  dia2dimlem12  36681  dia2dimlem13  36682  dvhopvadd  36699  dvhvaddass  36703  dvhopvsca  36708  tendolinv  36711  tendorinv  36712  dvhlveclem  36714  dvh0g  36717  dvheveccl  36718  dvhopN  36722  docaclN  36730  diaocN  36731  djajN  36743  dib0  36770  dib1dim  36771  dibglbN  36772  dibintclN  36773  dib1dim2  36774  diblss  36776  diblsmopel  36777  dicvaddcl  36796  dicvscacl  36797  diclspsn  36800  cdlemn4a  36805  cdlemn11c  36815  dihjustlem  36822  dihord1  36824  dihord2a  36825  dihord2b  36826  dihord2cN  36827  dihord11b  36828  dihord11c  36830  dihord2pre  36831  dihlsscpre  36840  dih1dimb  36846  dib2dim  36849  dih2dimb  36850  dih2dimbALTN  36851  dihvalcq2  36853  dihopelvalcpre  36854  dihord6apre  36862  dihord5b  36865  dihord5apre  36868  dih0  36886  dihmeetlem1N  36896  dihglblem5apreN  36897  dihglblem3N  36901  dihmeetlem2N  36905  dihglbcpreN  36906  dihmeetlem4preN  36912  dih1dimatlem0  36934  dih1dimatlem  36935  dihatlat  36940  dihatexv  36944  dihglb2  36948  dihmeet  36949  dihintcl  36950  dihmeet2  36952  doch2val2  36970  dochocss  36972  dihoml4c  36982  dochdmj1  36996  djhlj  37007  djhljjN  37008  djhjlj  37009  dihsumssj  37014  djhexmid  37017  djhlsmcl  37020  djhcvat42  37021  dihjatcclem4  37027  dihjat1lem  37034  dihsmsprn  37036  dihjat3  37038  dvh3dim2  37054  dvh3dim3N  37055  dochkr1OLDN  37085  lclkrlem2c  37115  lclkrlem2d  37116  mapdpglem23  37300  hdmap11lem2  37451  mzpcompact2lem  37631  diophrw  37639  rexrabdioph  37675  eldioph4b  37692  pellexlem5  37714  pellfund14  37779  acongtr  37862  fnwe2lem3  37939  gicabl  37986  hbtlem2  38011  hbtlem4  38013  hbtlem5  38015  dgraalem  38032  aaitgo  38049  ioounsn  38112  ntrclsk13  38686  gneispb  38746  wessf1ornlem  39685  ltdiv23neg  39930  islptre  40169  limclner  40201  icccncfext  40418  stoweidlem1  40536  stoweidlem14  40549  stoweidlem24  40559  stoweidlem46  40581  stoweidlem57  40592  dirkercncflem2  40639  fourierdlem20  40662  fourierdlem41  40683  fourierdlem46  40687  fourierdlem48  40689  fourierdlem50  40691  fourierdlem62  40703  fourierdlem63  40704  fourierdlem64  40705  fourierdlem65  40706  fourierdlem76  40717  fourierdlem79  40720  fourierdlem103  40744  fourierdlem104  40745  etransclem47  40816  raaan2  41496  iccpartiun  41695  sqrtpwpw2p  41775  fmtnoprmfac1lem  41801  fmtnoprmfac2lem1  41803  lighneallem4a  41850  perfectALTV  41957  nnsum4primeseven  42013  nnsum4primesevenALTV  42014  mgmpropd  42100  lidlmmgm  42250  gsumlsscl  42489  lincsumcl  42545  lincscmcl  42546  isldepslvec2  42599  m1modmmod  42641  elbigo2  42671  relogbdivb  42681  blennnt2  42708  dignn0ldlem  42721
  Copyright terms: Public domain W3C validator