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

Theorem syl12anc 835
 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 515 . 2 (𝜑 → (𝜒𝜃))
5 syl12anc.4 . 2 ((𝜓 ∧ (𝜒𝜃)) → 𝜏)
61, 4, 5syl2anc 587 1 (𝜑𝜏)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399 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 210  df-an 400 This theorem is referenced by:  syl22anc  837  raaan  4418  raaanv  4419  raaan2  4422  soltmin  5963  xpdifid  5992  reuop  6112  f1dom3fv3dif  7004  f1prex  7018  cocan1  7025  fliftfun  7044  soisores  7059  soisoi  7060  isopolem  7077  f1oiso2  7084  weniso  7086  caovcld  7322  caovcomd  7325  onminex  7504  tfrlem12  8010  omeulem1  8193  oaabs2  8257  omabs  8259  erov  8379  findcard2d  8746  frfi  8749  finsschain  8817  suplub2  8911  supgtoreq  8920  supisolem  8923  ordiso2  8965  ordtypelem7  8974  wemaplem2  8997  wemapsolem  9000  cantnflt  9121  cantnfp1lem3  9129  cantnflem1b  9135  cantnflem1  9138  wemapwe  9146  cnfcomlem  9148  cnfcom  9149  cnfcom3lem  9152  infxpenlem  9426  fseqenlem1  9437  dfac12lem2  9557  infpssrlem4  9719  enfin2i  9734  isf34lem7  9792  isf34lem6  9793  fin1a2lem7  9819  fin1a2lem10  9822  fin1a2lem11  9823  fin1a2lem13  9825  ttukeylem6  9927  ttukeylem7  9928  iundom2g  9953  fpwwe2lem5  10048  fpwwe2lem6  10049  fpwwe2lem8  10051  fpwwe2lem11  10054  fpwwe2  10056  canthnumlem  10061  canthwelem  10063  canthp1lem2  10066  pwfseqlem4  10075  inar1  10188  intgru  10227  distrlem4pr  10439  conjmul  11348  lediv12a  11524  recp1lt1  11529  cju  11623  gtndiv  12049  zsupss  12327  uzsupss  12330  icc0  12776  iccssioo2  12800  fzrev3  12970  ico01fl0  13186  fldiv  13225  modabs  13269  modltm1p1mod  13288  modifeq2int  13298  modsumfzodifsn  13309  seqcaopr  13405  seqf1olem1  13407  seqof2  13426  crreczi  13587  seqcoll  13820  seqcoll2  13821  hashtpg  13841  swrdccat3b  14095  sqrlem2  14597  resqrex  14604  abs1m  14689  isercoll  15018  zsum  15069  fsum2dlem  15119  fsumcom2  15123  fprod2dlem  15328  fprodcom2  15332  efsub  15447  bitsinv2  15784  sqgcd  15901  qredeu  15994  isprm7  16044  pcpremul  16172  pceulem  16174  pczpre  16176  pcdiv  16181  pcqmul  16182  pcqdiv  16186  pcexp  16188  pcdvdsb  16197  pcneg  16202  pcdvdstr  16204  pcgcd1  16205  pc2dvds  16207  pcz  16209  pcaddlem  16216  pcadd  16217  qexpz  16229  expnprm  16230  infpnlem2  16239  ramub2  16342  ramub1lem1  16354  setsstruct2  16515  f1ocpbllem  16791  f1ovscpbl  16793  mreexexlem3d  16911  mreexexlem4d  16912  fthi  17182  ipodrsima  17769  mndpropd  17930  grpsubpropd2  18200  ghmf1  18382  symgfvne  18504  f1omvdmvd  18566  f1otrspeq  18570  pmtrdifwrdel  18608  pmtrdifwrdel2  18609  psgnunilem2  18618  psgnunilem3  18619  psgnvalii  18632  odf1  18684  lsmpropd  18798  ablnnncan  18939  gsummptshft  19052  dprdf1o  19150  pgpfac1lem3  19195  pgpfac1lem5  19197  pgpfaclem1  19199  ablfaclem2  19204  srgbinomlem3  19288  ringpropd  19331  f1ghm0to0  19491  lmodprop2d  19692  lsspropd  19785  lmhmpropd  19841  lbspropd  19867  lbsextlem3  19928  iporthcom  20328  obslbs  20423  assapropd  20562  psrass1  20647  psrass23l  20650  psrass23  20652  mplsubrg  20682  mplmon  20707  mplmonmul  20708  mplcoe1  20709  mplbas2  20714  mplind  20745  evlslem2  20755  mpfind  20783  gsumply1subr  20870  psrplusgpropd  20872  ply1scln0  20927  scmataddcl  21128  scmatsubcl  21129  scmatmulcl  21130  smatvscl  21136  scmatrhmcl  21140  mat1scmat  21151  smadiadetglem2  21284  cramerimplem2  21296  cramerimplem3  21297  cramerimp  21298  1pmatscmul  21314  mat2pmatf1  21341  pm2mp  21437  chmatcl  21440  chmatval  21441  chmaidscmat  21460  chfacfisf  21466  cayhamlem1  21478  cpmidgsumm2pm  21481  cpmidpmat  21485  cpmadugsumfi  21489  cpmadumatpoly  21495  cayhamlem3  21499  pptbas  21620  elcls  21685  neiint  21716  neiptopnei  21744  restbas  21770  neitr  21792  iscnp4  21875  cnconst2  21895  cnpdis  21905  cnt0  21958  cnhaus  21966  cmpcovf  22003  hauscmplem  22018  conncompid  22043  2ndci  22060  2ndc1stc  22063  1stcrest  22065  2ndcctbss  22067  2ndcomap  22070  2ndcsep  22071  dis2ndc  22072  restlly  22095  islly2  22096  lly1stc  22108  dislly  22109  finlocfin  22132  dissnlocfin  22141  locfindis  22142  llycmpkgen2  22162  ptbasfi  22193  neitx  22219  ptpjopn  22224  ptcnplem  22233  upxp  22235  txlly  22248  txtube  22252  tx1stc  22262  txkgen  22264  xkococnlem  22271  kqreglem1  22353  kqreglem2  22354  kqnrmlem1  22355  kqnrmlem2  22356  hmeoimaf1o  22382  reghmph  22405  nrmhmph  22406  ordthmeolem  22413  trfil2  22499  fmfnfm  22570  hauspwpwf1  22599  fclsfnflim  22639  cnextf  22678  cnextcn  22679  tmdgsum2  22708  symgtgp  22718  subgntr  22719  opnsubg  22720  ghmcnp  22727  qustgpopn  22732  tsmsf1o  22757  tsmsxplem1  22765  tsmsxplem2  22766  tsmsxp  22767  ustexsym  22828  restutop  22850  imasdsf1olem  22987  blssexps  23040  blssex  23041  ssblex  23042  imasf1oxms  23103  blcld  23119  stdbdmopn  23132  met1stc  23135  met2ndci  23136  prdsxmslem2  23143  metcnp3  23154  cfilucfil  23173  ngptgp  23249  tgioo  23408  tgqioo  23412  zdis  23428  iccpnfhmeo  23557  xrhmeo  23558  cnheibor  23567  elpi1i  23658  cmetcusp  23965  bncssbn  23985  pjthlem2  24049  ivthlem2  24063  ovolicc1  24127  ovolicc2lem3  24130  ovolicc2lem4  24131  volsup  24167  volivth  24218  vitalilem3  24221  mbflimsup  24277  mbfi1fseqlem1  24326  mbfi1fseqlem3  24328  mbfi1fseqlem5  24330  limcnlp  24488  limcflf  24491  limciun  24504  dvmptfsum  24585  dvcnvlem  24586  dvcvx  24630  facth1  24772  elply2  24800  plypf1  24816  coeeq  24831  aaliou3lem8  24948  ulm2  24987  mtestbdd  25007  reeff1o  25049  logbgcd1irr  25387  dcubic2  25437  quart  25454  xrlimcnp  25561  amgm  25583  harmonicbnd4  25603  perfect  25822  dchrptlem1  25855  bposlem2  25876  lgsfcl2  25894  lgsdir  25923  lgsdi  25925  lgsne0  25926  2lgslem1a1  25980  2sqmod  26027  dchrvmasumlem2  26089  chpdifbndlem2  26145  pntpbnd1  26177  pntpbnd2  26178  padicabv  26221  tgcgrxfr  26319  idmot  26338  legid  26388  btwnleg  26389  leg0  26393  tghilberti1  26438  mirreu3  26455  colperpex  26534  lnopp2hpgb  26564  axcgrrflx  26715  axsegconlem1  26718  axcontlem2  26766  axcontlem12  26776  eengtrkg  26787  wwlksnredwwlkn  27688  0wlkon  27912  0trlon  27916  upgr3v3e3cycl  27972  frgrogt3nreg  28189  nvpi  28457  nmlno0lem  28583  fh1  29408  fh2  29409  nmlnop0iALT  29785  nmopun  29804  branmfn  29895  opsqrlem1  29930  opsqrlem6  29935  mdslmd1lem1  30115  csmdsymi  30124  atom1d  30143  chirredlem2  30181  cdj1i  30223  cdj3i  30231  fcnvgreu  30443  suppovss  30450  xrofsup  30525  pwrssmgc  30713  gsummpt2d  30741  gsumhashmul  30748  odpmco  30787  cycpmco2lem6  30830  cycpmco2  30832  cyc3evpm  30849  cycpmconjslem2  30854  archirngz  30875  archiabllem2a  30880  orngsqr  30935  ornglmullt  30938  orngrmullt  30939  lindssn  31000  lindfpropd  31003  ssmxidllem  31056  lindsun  31121  dimkerim  31123  fedgmullem2  31126  metideq  31258  metider  31259  pstmfval  31261  lmxrge0  31317  qqhval2  31345  qqhf  31349  qqhghm  31351  qqhrhm  31352  esumpcvgval  31459  esum2dlem  31473  esum2d  31474  sigainb  31517  insiga  31518  ddemeas  31617  imambfm  31642  dya2icoseg  31657  dya2iocnrect  31661  eulerpartlemgvv  31756  probun  31799  ballotlemfc0  31872  ballotlemfcc  31873  sgnmul  31922  breprexplemc  32025  erdszelem8  32570  erdszelem9  32571  erdsze2lem2  32576  cnpconn  32602  txpconn  32604  ptpconn  32605  indispconn  32606  connpconn  32607  cvxpconn  32614  cnllysconn  32617  cvmcov2  32647  cvmopnlem  32650  cvmliftmolem1  32653  cvmliftlem14  32669  cvmliftlem15  32670  cvmlift2lem13  32687  cvmlift3lem2  32692  cvmlift3lem9  32699  poseq  33220  sltres  33294  nolesgn2o  33303  nodense  33321  nosupbnd1lem3  33335  nosupbnd1lem5  33337  nosupbnd2lem1  33340  nocvxmin  33373  seglerflx  33698  seglemin  33699  btwnsegle  33703  hilbert1.1  33740  neibastop2lem  33833  bj-finsumval0  34716  relowlssretop  34796  wl-2sb6d  34975  tan2h  35065  poimirlem1  35074  poimirlem3  35076  poimirlem4  35077  poimirlem9  35082  poimirlem22  35095  poimirlem28  35101  heicant  35108  mblfinlem2  35111  itg2addnc  35127  ftc2nc  35155  dvasin  35157  sdclem1  35197  fdc  35199  istotbnd3  35225  sstotbnd  35229  prdstotbnd  35248  prdsbnd2  35249  cntotbnd  35250  rngoisocnv  35435  lsmsat  36320  islfld  36374  ps-2  36790  lplnexllnN  36876  4atlem9  36915  4atlem10a  36916  lnatexN  37091  2lnat  37096  pmapjat1  37165  lhpj1  37334  lhpm0atN  37341  4atexlemex2  37383  4atex  37388  4atex2-0aOLDN  37390  4atex2-0cOLDN  37392  lautcnvle  37401  lautj  37405  lautm  37406  idltrn  37462  cdleme01N  37533  cdleme0ex1N  37535  cdleme5  37552  cdleme9  37565  cdleme11c  37573  cdleme11g  37577  cdlemefrs29bpre0  37708  cdlemefrs29cpre1  37710  cdlemefrs32fva1  37713  cdleme32fva  37749  cdleme32fva1  37750  cdleme32fvaw  37751  cdleme32d  37756  cdleme32f  37758  cdleme35fnpq  37761  cdleme48d  37847  cdleme48gfv  37849  cdleme50ltrn  37869  trlord  37881  cdlemg4b1  37921  cdlemg4b2  37922  cdlemg13a  37963  cdlemg17a  37973  cdlemg17f  37978  erng1lem  38299  erngdvlem3  38302  erngdvlem4  38303  erng1r  38307  erngdvlem3-rN  38310  erngdvlem4-rN  38311  dva0g  38339  dialss  38358  dia0  38364  dia1N  38365  diaglbN  38367  diameetN  38368  diainN  38369  diaintclN  38370  dia1dim  38373  dia2dimlem5  38380  dia2dimlem7  38382  dia2dimlem9  38384  dia2dimlem10  38385  dia2dimlem12  38387  dia2dimlem13  38388  dvhopvadd  38405  dvhvaddass  38409  dvhopvsca  38414  tendolinv  38417  tendorinv  38418  dvhlveclem  38420  dvh0g  38423  dvheveccl  38424  dvhopN  38428  docaclN  38436  diaocN  38437  djajN  38449  dib0  38476  dib1dim  38477  dibglbN  38478  dibintclN  38479  dib1dim2  38480  diblss  38482  diblsmopel  38483  dicvaddcl  38502  dicvscacl  38503  diclspsn  38506  cdlemn4a  38511  cdlemn11c  38521  dihjustlem  38528  dihord1  38530  dihord2a  38531  dihord2b  38532  dihord2cN  38533  dihord11b  38534  dihord11c  38536  dihord2pre  38537  dihlsscpre  38546  dih1dimb  38552  dib2dim  38555  dih2dimb  38556  dih2dimbALTN  38557  dihvalcq2  38559  dihopelvalcpre  38560  dihord6apre  38568  dihord5b  38571  dihord5apre  38574  dih0  38592  dihmeetlem1N  38602  dihglblem5apreN  38603  dihglblem3N  38607  dihmeetlem2N  38611  dihglbcpreN  38612  dihmeetlem4preN  38618  dih1dimatlem0  38640  dih1dimatlem  38641  dihatlat  38646  dihatexv  38650  dihglb2  38654  dihmeet  38655  dihintcl  38656  dihmeet2  38658  doch2val2  38676  dochocss  38678  dihoml4c  38688  dochdmj1  38702  djhlj  38713  djhljjN  38714  djhjlj  38715  dihsumssj  38720  djhexmid  38723  djhlsmcl  38726  djhcvat42  38727  dihjatcclem4  38733  dihjat1lem  38740  dihsmsprn  38742  dihjat3  38744  dvh3dim2  38760  dvh3dim3N  38761  dochkr1OLDN  38791  lclkrlem2c  38821  lclkrlem2d  38822  mapdpglem23  39006  hdmap11lem2  39154  expgcd  39506  0prjspn  39629  mzpcompact2lem  39707  diophrw  39715  rexrabdioph  39750  eldioph4b  39767  pellexlem5  39789  pellfund14  39854  acongtr  39934  fnwe2lem3  40011  gicabl  40058  hbtlem2  40083  hbtlem4  40085  hbtlem5  40087  dgraalem  40104  aaitgo  40121  ntrclsk13  40789  gneispb  40849  wessf1ornlem  41826  ltdiv23neg  42045  islptre  42276  limclner  42308  icccncfext  42544  stoweidlem1  42658  stoweidlem14  42671  stoweidlem24  42681  stoweidlem46  42703  stoweidlem57  42714  dirkercncflem2  42761  fourierdlem20  42784  fourierdlem41  42805  fourierdlem46  42809  fourierdlem48  42811  fourierdlem50  42813  fourierdlem62  42825  fourierdlem63  42826  fourierdlem64  42827  fourierdlem65  42828  fourierdlem76  42839  fourierdlem79  42842  fourierdlem103  42866  fourierdlem104  42867  etransclem47  42938  iccpartiun  43966  reupr  44054  sqrtpwpw2p  44070  fmtnoprmfac1lem  44096  fmtnoprmfac2lem1  44098  lighneallem4a  44141  requad2  44156  perfectALTV  44256  nnsum4primeseven  44333  nnsum4primesevenALTV  44334  mgmpropd  44410  lidlmmgm  44564  gsumlsscl  44800  lincsumcl  44854  lincscmcl  44855  isldepslvec2  44908  m1modmmod  44949  elbigo2  44980  relogbdivb  44990  blennnt2  45017  dignn0ldlem  45030  itsclc0yqsollem2  45191  inlinecirc02p  45215
 Copyright terms: Public domain W3C validator