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

Theorem syl12anc 1475
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 559 . 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  1478  raaan  4226  soltmin  5690  xpdifid  5720  f1dom3fv3dif  6688  f1prex  6702  cocan1  6709  fliftfun  6725  soisores  6740  soisoi  6741  isopolem  6758  f1oiso2  6765  weniso  6767  caovcld  6992  caovcomd  6995  onminex  7172  tfrlem12  7654  omeulem1  7831  oaabs2  7894  omabs  7896  erov  8011  findcard2d  8367  frfi  8370  finsschain  8438  suplub2  8532  supgtoreq  8541  supisolem  8544  ordiso2  8585  ordtypelem7  8594  wemaplem2  8617  wemapsolem  8620  cantnflt  8742  cantnfp1lem3  8750  cantnflem1b  8756  cantnflem1  8759  wemapwe  8767  cnfcomlem  8769  cnfcom  8770  cnfcom3lem  8773  infxpenlem  9026  fseqenlem1  9037  dfac12lem2  9158  infpssrlem4  9320  enfin2i  9335  isf34lem7  9393  isf34lem6  9394  fin1a2lem7  9420  fin1a2lem10  9423  fin1a2lem11  9424  fin1a2lem13  9426  ttukeylem6  9528  ttukeylem7  9529  iundom2g  9554  fpwwe2lem6  9649  fpwwe2lem7  9650  fpwwe2lem9  9652  fpwwe2lem12  9655  fpwwe2  9657  canthnumlem  9662  canthwelem  9664  canthp1lem2  9667  pwfseqlem4  9676  inar1  9789  intgru  9828  distrlem4pr  10040  conjmul  10934  lediv12a  11108  recp1lt1  11113  cju  11208  gtndiv  11646  zsupss  11970  uzsupss  11973  icc0  12416  iccssioo2  12439  fzrev3  12599  ico01fl0  12814  fldiv  12853  modabs  12897  modltm1p1mod  12916  modifeq2int  12926  seqcaopr  13032  seqf1olem1  13034  seqof2  13053  crreczi  13183  seqcoll  13440  seqcoll2  13441  hashtpg  13459  swrdccat3b  13696  sqrlem2  14183  resqrex  14190  abs1m  14274  isercoll  14597  zsum  14648  fsum2dlem  14700  fsumcom2  14704  fsumcom2OLD  14705  fprod2dlem  14909  fprodcom2  14913  fprodcom2OLD  14914  efsub  15029  bitsinv2  15367  sqgcd  15480  qredeu  15574  isprm7  15622  pcpremul  15750  pceulem  15752  pczpre  15754  pcdiv  15759  pcqmul  15760  pcqdiv  15764  pcexp  15766  pcdvdsb  15775  pcneg  15780  pcdvdstr  15782  pcgcd1  15783  pc2dvds  15785  pcz  15787  pcaddlem  15794  pcadd  15795  qexpz  15807  expnprm  15808  infpnlem2  15817  ramub2  15920  ramub1lem1  15932  setsstruct2  16098  f1ocpbllem  16386  f1ovscpbl  16388  mreexexlem3d  16508  mreexexlem4d  16509  fthi  16779  ipodrsima  17366  mndpropd  17517  grpsubpropd2  17722  ghmf1  17890  symgfvne  18008  f1omvdmvd  18063  f1otrspeq  18067  pmtrdifwrdel  18105  pmtrdifwrdel2  18106  psgnunilem2  18115  psgnunilem3  18116  psgnvalii  18129  odf1  18179  lsmpropd  18290  ablnnncan  18428  gsummptshft  18536  dprdf1o  18631  pgpfac1lem3  18676  pgpfac1lem5  18678  pgpfaclem1  18680  ablfaclem2  18685  srgbinomlem3  18742  ringpropd  18782  f1rhm0to0  18942  lmodprop2d  19127  lsspropd  19219  lmhmpropd  19275  lbspropd  19301  lbsextlem3  19362  assapropd  19529  psrass1  19607  psrass23l  19610  psrass23  19612  mplsubrg  19642  mplmon  19665  mplmonmul  19666  mplcoe1  19667  mplbas2  19672  mplind  19704  evlslem2  19714  mpfind  19738  gsumply1subr  19806  psrplusgpropd  19808  ply1scln0  19863  iporthcom  20182  obslbs  20276  scmataddcl  20524  scmatsubcl  20525  scmatmulcl  20526  smatvscl  20532  scmatrhmcl  20536  mat1scmat  20547  smadiadetglem2  20680  cramerimplem2  20692  cramerimplem3  20693  cramerimp  20694  1pmatscmul  20709  mat2pmatf1  20736  pm2mp  20832  chmatcl  20835  chmatval  20836  chmaidscmat  20855  chfacfisf  20861  cayhamlem1  20873  cpmidgsumm2pm  20876  cpmidpmat  20880  cpmadugsumfi  20884  cpmadumatpoly  20890  cayhamlem3  20894  pptbas  21014  elcls  21079  neiint  21110  neiptopnei  21138  restbas  21164  neitr  21186  iscnp4  21269  cnconst2  21289  cnpdis  21299  cnt0  21352  cnhaus  21360  cmpcovf  21396  hauscmplem  21411  conncompid  21436  2ndci  21453  2ndc1stc  21456  1stcrest  21458  2ndcctbss  21460  2ndcomap  21463  2ndcsep  21464  dis2ndc  21465  restlly  21488  islly2  21489  lly1stc  21501  dislly  21502  finlocfin  21525  dissnlocfin  21534  locfindis  21535  llycmpkgen2  21555  ptbasfi  21586  neitx  21612  ptpjopn  21617  ptcnplem  21626  upxp  21628  txlly  21641  txtube  21645  tx1stc  21655  txkgen  21657  xkococnlem  21664  kqreglem1  21746  kqreglem2  21747  kqnrmlem1  21748  kqnrmlem2  21749  hmeoimaf1o  21775  reghmph  21798  nrmhmph  21799  ordthmeolem  21806  trfil2  21892  fmfnfm  21963  hauspwpwf1  21992  fclsfnflim  22032  cnextf  22071  cnextcn  22072  tmdgsum2  22101  symgtgp  22106  subgntr  22111  opnsubg  22112  ghmcnp  22119  qustgpopn  22124  tsmsf1o  22149  tsmsxplem1  22157  tsmsxplem2  22158  tsmsxp  22159  ustexsym  22220  restutop  22242  imasdsf1olem  22379  blssexps  22432  blssex  22433  ssblex  22434  imasf1oxms  22495  blcld  22511  stdbdmopn  22524  met1stc  22527  met2ndci  22528  prdsxmslem2  22535  metcnp3  22546  cfilucfil  22565  ngptgp  22641  tgioo  22800  tgqioo  22804  zdis  22820  iccpnfhmeo  22945  xrhmeo  22946  cnheibor  22955  elpi1i  23046  cmetcusp  23350  pjthlem2  23409  ivthlem2  23421  ovolicc1  23484  ovolicc2lem3  23487  ovolicc2lem4  23488  volsup  23524  volivth  23575  vitalilem3  23578  mbflimsup  23632  mbfi1fseqlem1  23681  mbfi1fseqlem3  23683  mbfi1fseqlem5  23685  limcnlp  23841  limcflf  23844  limciun  23857  dvmptfsum  23937  dvcnvlem  23938  dvcvx  23982  facth1  24123  elply2  24151  plypf1  24167  coeeq  24182  aaliou3lem8  24299  ulm2  24338  mtestbdd  24358  reeff1o  24400  dcubic2  24770  quart  24787  xrlimcnp  24894  amgm  24916  harmonicbnd4  24936  perfect  25155  dchrptlem1  25188  bposlem2  25209  lgsfcl2  25227  lgsdir  25256  lgsdi  25258  lgsne0  25259  2lgslem1a1  25313  dchrvmasumlem2  25386  chpdifbndlem2  25442  pntpbnd1  25474  pntpbnd2  25475  padicabv  25518  tgcgrxfr  25612  idmot  25631  legid  25681  btwnleg  25682  leg0  25686  tghilberti1  25731  mirreu3  25748  colperpex  25824  lnopp2hpgb  25854  axcgrrflx  25993  axsegconlem1  25996  axcontlem2  26044  axcontlem12  26054  eengtrkg  26064  wwlksnredwwlkn  27013  clwwlkel  27175  clwlksfclwwlkOLD  27216  clwwlknonex2lem2  27257  0wlkon  27272  0trlon  27276  upgr3v3e3cycl  27332  frgrogt3nreg  27565  nvpi  27831  nmlno0lem  27957  fh1  28786  fh2  28787  eigposi  29004  nmlnop0iALT  29163  nmopun  29182  branmfn  29273  opsqrlem1  29308  opsqrlem6  29313  mdslmd1lem1  29493  csmdsymi  29502  atom1d  29521  chirredlem2  29559  cdj1i  29601  cdj3i  29609  fcnvgreu  29781  xrofsup  29842  2sqmod  29957  archirngz  30052  archiabllem2a  30057  gsummpt2d  30090  orngsqr  30113  ornglmullt  30116  orngrmullt  30117  metideq  30245  metider  30246  pstmfval  30248  lmxrge0  30307  qqhval2  30335  qqhf  30339  qqhghm  30341  qqhrhm  30342  esumpcvgval  30449  esum2dlem  30463  esum2d  30464  sigainb  30508  insiga  30509  ddemeas  30608  imambfm  30633  dya2icoseg  30648  dya2iocnrect  30652  eulerpartlemgvv  30747  probun  30790  ballotlemfc0  30863  ballotlemfcc  30864  sgnmul  30913  signstfvneq0  30958  breprexplemc  31019  erdszelem8  31487  erdszelem9  31488  erdsze2lem2  31493  cnpconn  31519  txpconn  31521  ptpconn  31522  indispconn  31523  connpconn  31524  cvxpconn  31531  cnllysconn  31534  cvmcov2  31564  cvmopnlem  31567  cvmliftmolem1  31570  cvmliftlem14  31586  cvmliftlem15  31587  cvmlift2lem13  31604  cvmlift3lem2  31609  cvmlift3lem9  31616  poseq  32059  sltres  32121  nolesgn2o  32130  nodense  32148  nosupbnd1lem3  32162  nosupbnd1lem5  32164  nosupbnd2lem1  32167  nocvxmin  32200  seglerflx  32525  seglemin  32526  btwnsegle  32530  hilbert1.1  32567  neibastop2lem  32661  bj-finsumval0  33458  relowlssretop  33522  wl-2sb6d  33654  tan2h  33714  poimirlem1  33723  poimirlem3  33725  poimirlem4  33726  poimirlem9  33731  poimirlem22  33744  poimirlem28  33750  heicant  33757  mblfinlem2  33760  itg2addnc  33777  ftc2nc  33807  dvasin  33809  sdclem1  33852  fdc  33854  istotbnd3  33883  sstotbnd  33887  prdstotbnd  33906  prdsbnd2  33907  cntotbnd  33908  rngoisocnv  34093  lsmsat  34798  islfld  34852  ps-2  35267  lplnexllnN  35353  4atlem9  35392  4atlem10a  35393  lnatexN  35568  2lnat  35573  pmapjat1  35642  lhpj1  35811  lhpm0atN  35818  4atexlemex2  35860  4atex  35865  4atex2-0aOLDN  35867  4atex2-0cOLDN  35869  lautcnvle  35878  lautj  35882  lautm  35883  idltrn  35939  cdleme01N  36011  cdleme0ex1N  36013  cdleme5  36030  cdleme9  36043  cdleme11c  36051  cdleme11g  36055  cdlemefrs29bpre0  36186  cdlemefrs29cpre1  36188  cdlemefrs32fva1  36191  cdleme32fva  36227  cdleme32fva1  36228  cdleme32fvaw  36229  cdleme32d  36234  cdleme32f  36236  cdleme35fnpq  36239  cdleme48d  36325  cdleme48gfv  36327  cdleme50ltrn  36347  trlord  36359  cdlemg4b1  36399  cdlemg4b2  36400  cdlemg13a  36441  cdlemg17a  36451  cdlemg17f  36456  erng1lem  36777  erngdvlem3  36780  erngdvlem4  36781  erng1r  36785  erngdvlem3-rN  36788  erngdvlem4-rN  36789  dva0g  36818  dialss  36837  dia0  36843  dia1N  36844  diaglbN  36846  diameetN  36847  diainN  36848  diaintclN  36849  dia1dim  36852  dia2dimlem5  36859  dia2dimlem7  36861  dia2dimlem9  36863  dia2dimlem10  36864  dia2dimlem12  36866  dia2dimlem13  36867  dvhopvadd  36884  dvhvaddass  36888  dvhopvsca  36893  tendolinv  36896  tendorinv  36897  dvhlveclem  36899  dvh0g  36902  dvheveccl  36903  dvhopN  36907  docaclN  36915  diaocN  36916  djajN  36928  dib0  36955  dib1dim  36956  dibglbN  36957  dibintclN  36958  dib1dim2  36959  diblss  36961  diblsmopel  36962  dicvaddcl  36981  dicvscacl  36982  diclspsn  36985  cdlemn4a  36990  cdlemn11c  37000  dihjustlem  37007  dihord1  37009  dihord2a  37010  dihord2b  37011  dihord2cN  37012  dihord11b  37013  dihord11c  37015  dihord2pre  37016  dihlsscpre  37025  dih1dimb  37031  dib2dim  37034  dih2dimb  37035  dih2dimbALTN  37036  dihvalcq2  37038  dihopelvalcpre  37039  dihord6apre  37047  dihord5b  37050  dihord5apre  37053  dih0  37071  dihmeetlem1N  37081  dihglblem5apreN  37082  dihglblem3N  37086  dihmeetlem2N  37090  dihglbcpreN  37091  dihmeetlem4preN  37097  dih1dimatlem0  37119  dih1dimatlem  37120  dihatlat  37125  dihatexv  37129  dihglb2  37133  dihmeet  37134  dihintcl  37135  dihmeet2  37137  doch2val2  37155  dochocss  37157  dihoml4c  37167  dochdmj1  37181  djhlj  37192  djhljjN  37193  djhjlj  37194  dihsumssj  37199  djhexmid  37202  djhlsmcl  37205  djhcvat42  37206  dihjatcclem4  37212  dihjat1lem  37219  dihsmsprn  37221  dihjat3  37223  dvh3dim2  37239  dvh3dim3N  37240  dochkr1OLDN  37270  lclkrlem2c  37300  lclkrlem2d  37301  mapdpglem23  37485  hdmap11lem2  37636  mzpcompact2lem  37816  diophrw  37824  rexrabdioph  37860  eldioph4b  37877  pellexlem5  37899  pellfund14  37964  acongtr  38047  fnwe2lem3  38124  gicabl  38171  hbtlem2  38196  hbtlem4  38198  hbtlem5  38200  dgraalem  38217  aaitgo  38234  ioounsn  38297  ntrclsk13  38871  gneispb  38931  wessf1ornlem  39870  ltdiv23neg  40115  islptre  40354  limclner  40386  icccncfext  40603  stoweidlem1  40721  stoweidlem14  40734  stoweidlem24  40744  stoweidlem46  40766  stoweidlem57  40777  dirkercncflem2  40824  fourierdlem20  40847  fourierdlem41  40868  fourierdlem46  40872  fourierdlem48  40874  fourierdlem50  40876  fourierdlem62  40888  fourierdlem63  40889  fourierdlem64  40890  fourierdlem65  40891  fourierdlem76  40902  fourierdlem79  40905  fourierdlem103  40929  fourierdlem104  40930  etransclem47  41001  raaan2  41681  iccpartiun  41880  sqrtpwpw2p  41960  fmtnoprmfac1lem  41986  fmtnoprmfac2lem1  41988  lighneallem4a  42035  perfectALTV  42142  nnsum4primeseven  42198  nnsum4primesevenALTV  42199  mgmpropd  42285  lidlmmgm  42435  gsumlsscl  42674  lincsumcl  42730  lincscmcl  42731  isldepslvec2  42784  m1modmmod  42826  elbigo2  42856  relogbdivb  42866  blennnt2  42893  dignn0ldlem  42906
  Copyright terms: Public domain W3C validator