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

Theorem syl12anc 1316
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 556 . 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 196  df-an 385
This theorem is referenced by:  syl22anc  1319  raaan  4032  soltmin  5451  xpdifid  5481  f1dom3fv3dif  6425  f1prex  6439  cocan1  6446  fliftfun  6462  soisores  6477  soisoi  6478  isopolem  6495  f1oiso2  6502  weniso  6504  caovcld  6725  caovcomd  6728  onminex  6899  tfrlem12  7372  omeulem1  7549  oaabs2  7612  omabs  7614  erov  7731  findcard2d  8087  frfi  8090  finsschain  8156  suplub2  8250  supgtoreq  8259  supisolem  8262  ordiso2  8303  ordtypelem7  8312  wemaplem2  8335  wemapsolem  8338  cantnflt  8452  cantnfp1lem3  8460  cantnflem1b  8466  cantnflem1  8469  wemapwe  8477  cnfcomlem  8479  cnfcom  8480  cnfcom3lem  8483  infxpenlem  8719  fseqenlem1  8730  dfac12lem2  8849  infpssrlem4  9011  enfin2i  9026  isf34lem7  9084  isf34lem6  9085  fin1a2lem7  9111  fin1a2lem10  9114  fin1a2lem11  9115  fin1a2lem13  9117  ttukeylem6  9219  ttukeylem7  9220  iundom2g  9241  fpwwe2lem6  9336  fpwwe2lem7  9337  fpwwe2lem9  9339  fpwwe2lem12  9342  fpwwe2  9344  canthnumlem  9349  canthwelem  9351  canthp1lem2  9354  pwfseqlem4  9363  inar1  9476  intgru  9515  distrlem4pr  9727  conjmul  10621  lediv12a  10795  recp1lt1  10800  cju  10893  gtndiv  11330  zsupss  11653  uzsupss  11656  icc0  12094  iccssioo2  12117  fzrev3  12276  elfz1b  12279  ico01fl0  12482  fldiv  12521  modabs  12565  modltm1p1mod  12584  modifeq2int  12594  seqcaopr  12700  seqf1olem1  12702  seqof2  12721  crreczi  12851  seqcoll  13105  seqcoll2  13106  hashtpg  13121  swrdccat3b  13347  sqrlem2  13832  resqrex  13839  abs1m  13923  isercoll  14246  zsum  14296  fsum2dlem  14343  fsumcom2  14347  fsumcom2OLD  14348  fprod2dlem  14549  fprodcom2  14553  fprodcom2OLD  14554  efsub  14669  bitsinv2  15003  sqgcd  15116  qredeu  15210  isprm7  15258  pcpremul  15386  pceulem  15388  pczpre  15390  pcdiv  15395  pcqmul  15396  pcqdiv  15400  pcexp  15402  pcdvdsb  15411  pcneg  15416  pcdvdstr  15418  pcgcd1  15419  pc2dvds  15421  pcz  15423  pcaddlem  15430  pcadd  15431  qexpz  15443  expnprm  15444  infpnlem2  15453  ramub2  15556  ramub1lem1  15568  f1ocpbllem  16007  f1ovscpbl  16009  mreexexlem3d  16129  mreexexlem4d  16130  fthi  16401  ipodrsima  16988  mndpropd  17139  grpsubpropd2  17344  ghmf1  17512  symgfvne  17631  f1omvdmvd  17686  f1otrspeq  17690  pmtrdifwrdel  17728  pmtrdifwrdel2  17729  psgnunilem2  17738  psgnunilem3  17739  psgnvalii  17752  odf1  17802  lsmpropd  17913  ablnnncan  18051  gsummptshft  18159  dprdf1o  18254  pgpfac1lem3  18299  pgpfac1lem5  18301  pgpfaclem1  18303  ablfaclem2  18308  srgbinomlem3  18365  ringpropd  18405  f1rhm0to0  18563  lmodprop2d  18748  lsspropd  18838  lmhmpropd  18894  lbspropd  18920  lbsextlem3  18981  assapropd  19148  psrass1  19226  psrass23l  19229  psrass23  19231  mplsubrg  19261  mplmon  19284  mplmonmul  19285  mplcoe1  19286  mplbas2  19291  mplind  19323  evlslem2  19333  mpfind  19357  gsumply1subr  19425  psrplusgpropd  19427  ply1scln0  19482  iporthcom  19799  obslbs  19893  scmataddcl  20141  scmatsubcl  20142  scmatmulcl  20143  smatvscl  20149  scmatrhmcl  20153  mat1scmat  20164  smadiadetglem2  20297  cramerimplem2  20309  cramerimplem3  20310  cramerimp  20311  1pmatscmul  20326  mat2pmatf1  20353  pm2mp  20449  chmatcl  20452  chmatval  20453  chmaidscmat  20472  chfacfisf  20478  cayhamlem1  20490  cpmidgsumm2pm  20493  cpmidpmat  20497  cpmadugsumfi  20501  cpmadumatpoly  20507  cayhamlem3  20511  pptbas  20622  elcls  20687  neiint  20718  neiptopnei  20746  restbas  20772  neitr  20794  iscnp4  20877  cnconst2  20897  cnpdis  20907  cnt0  20960  cnhaus  20968  cmpcovf  21004  hauscmplem  21019  concompid  21044  2ndci  21061  2ndc1stc  21064  1stcrest  21066  2ndcctbss  21068  2ndcomap  21071  2ndcsep  21072  dis2ndc  21073  restlly  21096  islly2  21097  lly1stc  21109  dislly  21110  finlocfin  21133  dissnlocfin  21142  locfindis  21143  llycmpkgen2  21163  ptbasfi  21194  neitx  21220  ptpjopn  21225  ptcnplem  21234  upxp  21236  txlly  21249  txtube  21253  tx1stc  21263  txkgen  21265  xkococnlem  21272  kqreglem1  21354  kqreglem2  21355  kqnrmlem1  21356  kqnrmlem2  21357  hmeoimaf1o  21383  reghmph  21406  nrmhmph  21407  ordthmeolem  21414  trfil2  21501  fmfnfm  21572  hauspwpwf1  21601  fclsfnflim  21641  cnextf  21680  cnextcn  21681  tmdgsum2  21710  symgtgp  21715  subgntr  21720  opnsubg  21721  ghmcnp  21728  qustgpopn  21733  tsmsf1o  21758  tsmsxplem1  21766  tsmsxplem2  21767  tsmsxp  21768  ustexsym  21829  restutop  21851  imasdsf1olem  21988  blssexps  22041  blssex  22042  ssblex  22043  imasf1oxms  22104  blcld  22120  stdbdmopn  22133  met1stc  22136  met2ndci  22137  prdsxmslem2  22144  metcnp3  22155  cfilucfil  22174  ngptgp  22250  tgioo  22407  tgqioo  22411  zdis  22427  iccpnfhmeo  22552  xrhmeo  22553  cnheibor  22562  elpi1i  22654  cmetcusp  22958  pjthlem2  23017  ivthlem2  23028  ovolicc1  23091  ovolicc2lem3  23094  ovolicc2lem4  23095  volsup  23131  volivth  23181  vitalilem3  23185  mbflimsup  23239  mbfi1fseqlem1  23288  mbfi1fseqlem3  23290  mbfi1fseqlem5  23292  limcnlp  23448  limcflf  23451  limciun  23464  dvmptfsum  23542  dvcnvlem  23543  dvcvx  23587  facth1  23728  elply2  23756  plypf1  23772  coeeq  23787  aaliou3lem8  23904  ulm2  23943  mtestbdd  23963  reeff1o  24005  dcubic2  24371  quart  24388  xrlimcnp  24495  amgm  24517  harmonicbnd4  24537  perfect  24756  dchrptlem1  24789  bposlem2  24810  lgsfcl2  24828  lgsdir  24857  lgsdi  24859  lgsne0  24860  2lgslem1a1  24914  dchrvmasumlem2  24987  chpdifbndlem2  25043  pntpbnd1  25075  pntpbnd2  25076  padicabv  25119  tgcgrxfr  25213  idmot  25232  legid  25282  btwnleg  25283  leg0  25287  tghilberti1  25332  mirreu3  25349  colperpex  25425  lnopp2hpgb  25455  axcgrrflx  25594  axsegconlem1  25597  axcontlem2  25645  axcontlem12  25655  eengtrkg  25665  uhgrstrrepelem  25744  nbgraf1olem5  25974  wwlknredwwlkn  26254  clwwlkel  26321  clwlkfclwwlk  26371  2spotiundisj  26589  numclwwlkovf2ex  26613  frgraogt3nreg  26647  nvpi  26906  nmlno0lem  27032  fh1  27861  fh2  27862  eigposi  28079  nmlnop0iALT  28238  nmopun  28257  branmfn  28348  opsqrlem1  28383  opsqrlem6  28388  mdslmd1lem1  28568  csmdsymi  28577  atom1d  28596  chirredlem2  28634  cdj1i  28676  cdj3i  28684  fcnvgreu  28855  xrofsup  28923  2sqmod  28979  archirngz  29074  archiabllem2a  29079  gsummpt2d  29112  orngsqr  29135  ornglmullt  29138  orngrmullt  29139  metideq  29264  metider  29265  pstmfval  29267  lmxrge0  29326  qqhval2  29354  qqhf  29358  qqhghm  29360  qqhrhm  29361  esumpcvgval  29467  esum2dlem  29481  esum2d  29482  sigainb  29526  insiga  29527  ddemeas  29626  imambfm  29651  dya2icoseg  29666  dya2iocnrect  29670  eulerpartlemgvv  29765  probun  29808  ballotlemfc0  29881  ballotlemfcc  29882  sgnmul  29931  signstfvneq0  29975  erdszelem8  30434  erdszelem9  30435  erdsze2lem2  30440  cnpcon  30466  txpcon  30468  ptpcon  30469  indispcon  30470  conpcon  30471  cvxpcon  30478  cnllyscon  30481  cvmcov2  30511  cvmopnlem  30514  cvmliftmolem1  30517  cvmliftlem14  30533  cvmliftlem15  30534  cvmlift2lem13  30551  cvmlift3lem2  30556  cvmlift3lem9  30563  poseq  30994  sltres  31061  nodense  31088  nocvxmin  31090  nobndup  31099  nobnddown  31100  seglerflx  31389  seglemin  31390  btwnsegle  31394  hilbert1.1  31431  neibastop2lem  31525  bj-finsumval0  32324  relowlssretop  32387  wl-2sb6d  32520  tan2h  32571  poimirlem1  32580  poimirlem3  32582  poimirlem4  32583  poimirlem9  32588  poimirlem22  32601  poimirlem28  32607  heicant  32614  mblfinlem2  32617  itg2addnc  32634  ftc2nc  32664  dvasin  32666  sdclem1  32709  fdc  32711  istotbnd3  32740  sstotbnd  32744  prdstotbnd  32763  prdsbnd2  32764  cntotbnd  32765  rngoisocnv  32950  lsmsat  33313  islfld  33367  ps-2  33782  lplnexllnN  33868  4atlem9  33907  4atlem10a  33908  lnatexN  34083  2lnat  34088  pmapjat1  34157  lhpj1  34326  lhpm0atN  34333  4atexlemex2  34375  4atex  34380  4atex2-0aOLDN  34382  4atex2-0cOLDN  34384  lautcnvle  34393  lautj  34397  lautm  34398  idltrn  34454  cdleme01N  34526  cdleme0ex1N  34528  cdleme5  34545  cdleme9  34558  cdleme11c  34566  cdleme11g  34570  cdlemefrs29bpre0  34702  cdlemefrs29cpre1  34704  cdlemefrs32fva1  34707  cdleme32fva  34743  cdleme32fva1  34744  cdleme32fvaw  34745  cdleme32d  34750  cdleme32f  34752  cdleme35fnpq  34755  cdleme48d  34841  cdleme48gfv  34843  cdleme50ltrn  34863  trlord  34875  cdlemg4b1  34915  cdlemg4b2  34916  cdlemg13a  34957  cdlemg17a  34967  cdlemg17f  34972  erng1lem  35293  erngdvlem3  35296  erngdvlem4  35297  erng1r  35301  erngdvlem3-rN  35304  erngdvlem4-rN  35305  dva0g  35334  dialss  35353  dia0  35359  dia1N  35360  diaglbN  35362  diameetN  35363  diainN  35364  diaintclN  35365  dia1dim  35368  dia2dimlem5  35375  dia2dimlem7  35377  dia2dimlem9  35379  dia2dimlem10  35380  dia2dimlem12  35382  dia2dimlem13  35383  dvhopvadd  35400  dvhvaddass  35404  dvhopvsca  35409  tendolinv  35412  tendorinv  35413  dvhlveclem  35415  dvh0g  35418  dvheveccl  35419  dvhopN  35423  docaclN  35431  diaocN  35432  djajN  35444  dib0  35471  dib1dim  35472  dibglbN  35473  dibintclN  35474  dib1dim2  35475  diblss  35477  diblsmopel  35478  dicvaddcl  35497  dicvscacl  35498  diclspsn  35501  cdlemn4a  35506  cdlemn11c  35516  dihjustlem  35523  dihord1  35525  dihord2a  35526  dihord2b  35527  dihord2cN  35528  dihord11b  35529  dihord11c  35531  dihord2pre  35532  dihlsscpre  35541  dih1dimb  35547  dib2dim  35550  dih2dimb  35551  dih2dimbALTN  35552  dihvalcq2  35554  dihopelvalcpre  35555  dihord6apre  35563  dihord5b  35566  dihord5apre  35569  dih0  35587  dihmeetlem1N  35597  dihglblem5apreN  35598  dihglblem3N  35602  dihmeetlem2N  35606  dihglbcpreN  35607  dihmeetlem4preN  35613  dih1dimatlem0  35635  dih1dimatlem  35636  dihatlat  35641  dihatexv  35645  dihglb2  35649  dihmeet  35650  dihintcl  35651  dihmeet2  35653  doch2val2  35671  dochocss  35673  dihoml4c  35683  dochdmj1  35697  djhlj  35708  djhljjN  35709  djhjlj  35710  dihsumssj  35715  djhexmid  35718  djhlsmcl  35721  djhcvat42  35722  dihjatcclem4  35728  dihjat1lem  35735  dihsmsprn  35737  dihjat3  35739  dvh3dim2  35755  dvh3dim3N  35756  dochkr1OLDN  35786  lclkrlem2c  35816  lclkrlem2d  35817  mapdpglem23  36001  hdmap11lem2  36152  mzpcompact2lem  36332  diophrw  36340  rexrabdioph  36376  eldioph4b  36393  pellexlem5  36415  pellfund14  36480  acongtr  36563  fnwe2lem3  36640  gicabl  36687  hbtlem2  36713  hbtlem4  36715  hbtlem5  36717  dgraalem  36734  aaitgo  36751  ioounsn  36814  ntrclsk13  37389  gneispb  37449  wessf1ornlem  38366  ltdiv23neg  38558  islptre  38686  limclner  38718  icccncfext  38773  stoweidlem1  38894  stoweidlem14  38907  stoweidlem24  38917  stoweidlem46  38939  stoweidlem57  38950  dirkercncflem2  38997  fourierdlem20  39020  fourierdlem41  39041  fourierdlem46  39045  fourierdlem48  39047  fourierdlem50  39049  fourierdlem62  39061  fourierdlem63  39062  fourierdlem64  39063  fourierdlem65  39064  fourierdlem76  39075  fourierdlem79  39078  fourierdlem103  39102  fourierdlem104  39103  etransclem47  39174  raaan2  39824  iccpartiun  39972  sqrtpwpw2p  39988  fmtnoprmfac1lem  40014  fmtnoprmfac2lem1  40016  lighneallem4a  40063  perfectALTV  40166  nnsum4primeseven  40216  nnsum4primesevenALTV  40217  wwlksnredwwlkn  41101  clwwlksel  41221  clwlksfclwwlk  41269  0wlkOn  41288  0TrlOn  41292  upgr3v3e3cycl  41347  av-numclwwlkovf2ex  41517  av-frgraogt3nreg  41551  mgmpropd  41565  lidlmmgm  41715  gsumlsscl  41958  lincsumcl  42014  lincscmcl  42015  isldepslvec2  42068  m1modmmod  42110  elbigo2  42144  relogbdivb  42154  blennnt2  42181  dignn0ldlem  42194
  Copyright terms: Public domain W3C validator