MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl3anbrc Structured version   Unicode version

Theorem syl3anbrc 1190
Description: Syllogism inference. (Contributed by Mario Carneiro, 11-May-2014.)
Hypotheses
Ref Expression
syl3anbrc.1  |-  ( ph  ->  ps )
syl3anbrc.2  |-  ( ph  ->  ch )
syl3anbrc.3  |-  ( ph  ->  th )
syl3anbrc.4  |-  ( ta  <->  ( ps  /\  ch  /\  th ) )
Assertion
Ref Expression
syl3anbrc  |-  ( ph  ->  ta )

Proof of Theorem syl3anbrc
StepHypRef Expression
1 syl3anbrc.1 . . 3  |-  ( ph  ->  ps )
2 syl3anbrc.2 . . 3  |-  ( ph  ->  ch )
3 syl3anbrc.3 . . 3  |-  ( ph  ->  th )
41, 2, 33jca 1186 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
5 syl3anbrc.4 . 2  |-  ( ta  <->  ( ps  /\  ch  /\  th ) )
64, 5sylibr 216 1  |-  ( ph  ->  ta )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    /\ w3a 983
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 189  df-an 373  df-3an 985
This theorem is referenced by:  soisores  6231  limuni3  6691  onfununi  7066  smores2  7079  smoiso  7087  oelimcl  7307  iserd  7395  erinxp  7443  resixp  7563  undifixp  7564  alephval3  8543  fpwwe2lem12  9068  canthwelem  9077  canthwe  9078  r1limwun  9163  wunex2  9165  tskcard  9208  gruina  9245  nqerf  9357  nqerid  9360  eluzuzle  11169  uztrn  11177  nn0pzuz  11218  zsupss  11255  nn0ge2m1nnALT  11260  xov1plusxeqvd  11780  ige2m1fz  11886  0elfz  11891  elfz0addOLD  11894  uzsubfz0  11900  elfzmlbm  11902  difelfzle  11906  difelfznle  11907  elfzolt2b  11933  elfzolt3b  11934  elfzouz2  11936  fzossrbm1  11949  elfzo0  11958  eluzgtdifelfzo  11977  elfzodifsumelfzo  11981  fzonn0p1  11991  fzonn0p1p1  11993  elfzom1p1elfzo  11994  fzo0sn0fzo1  12002  ssfzo12bi  12007  ubmelm1fzo  12008  elfzonelfzo  12012  fzosplitprm1  12019  fzostep1  12022  injresinjlem  12025  flword2  12049  uzsup  12091  fsuppmapnn0fiub  12204  suppssfz  12207  1elfz0hash  12570  fzsdom2  12599  ccatrn  12731  swrdn0  12782  swrdtrcfv  12793  swrdtrcfv0  12794  swrdeq  12796  swrdtrcfvl  12802  swrdswrd  12812  swrdccatwrd  12820  wrdeqs1cat  12827  swrdccatin1  12835  swrdccat3  12844  swrdccatid  12849  repswswrd  12883  cshwidxmod  12901  cshw1  12917  cshwcsh2id  12923  swrds2  13014  2swrd2eqwrdeq  13022  ccat2s1fvwALT  13024  rexuzre  13409  limsupgre  13535  limsupgreOLD  13536  rlimclim1  13602  rlimclim  13603  climrlim2  13604  isercolllem1  13721  isercoll  13724  climcndslem1  13900  fallfacval4  14089  tanhbnd  14208  sinbnd2  14229  cosbnd2  14230  rpnnen2  14271  bitsfzolem  14400  bitsfzolemOLD  14401  bitsfzo  14402  bitsmod  14403  bitsfi  14404  bitsinv1lem  14408  bitsinv1  14409  smueqlem  14457  prmn2uzge3  14637  zgz  14870  gznegcl  14872  gzcjcl  14873  gzaddcl  14874  gzmulcl  14875  vdwlem9  14932  prmgaplem3  15016  prmgaplem4  15017  cshwshashlem2  15060  ismred  15501  isfuncd  15763  homdmcoa  15955  isdrs2  16177  fpwipodrs  16403  ipodrsima  16404  psss  16453  psssdm2  16454  sgrp2rid2ex  16654  subgid  16812  issubg2  16825  subsubg  16833  gaorber  16955  orbsta  16960  pmtrfconj  17100  psgnunilem2  17129  psgnunilem3  17130  psgnunilem4  17131  pgpfi1  17240  subgpgp  17242  pgpssslw  17259  subgslw  17261  sylow2alem2  17263  fislw  17270  sylow3lem3  17274  efgs1  17378  efgsp1  17380  efgsres  17381  efgredleme  17386  efgcpbllemb  17398  lt6abl  17522  telgsumfzs  17612  ablfac1eu  17699  isringd  17808  ringsrg  17812  ring1  17823  prdsringd  17833  subrgsubg  18007  islmodd  18090  islssd  18152  islss4  18178  gsummoncoe1  18891  gzrngunit  19026  expmhm  19028  zringunit  19054  prmirredlem  19056  znidomb  19124  isphld  19213  ocvocv  19226  ocvlss  19227  frlmlbs  19347  mp2pm2mplem4  19825  chfacfisf  19870  chfacfisfcpmat  19871  chfacfscmulfsupp  19875  chfacfpmmulfsupp  19879  chfacfpmmulgsum2  19881  2ndcctbss  20462  finlocfin  20527  dissnlocfin  20536  locfindis  20537  locfincf  20538  isfild  20865  infil  20870  neifil  20887  flimfcls  21033  istgp2  21098  oppgtmd  21104  oppgtgp  21105  distgp  21106  indistgp  21107  symgtgp  21108  submtmd  21111  subgtgp  21112  qustgplem  21127  prdstmdd  21130  prdstgpd  21131  tlmtgp  21202  isngp4  21617  subgngp  21635  ngptgp  21636  tngngp2  21652  nrgtrg  21684  nrgtdrg  21687  elii2  21956  icopnfcnv  21962  xrhmeo  21966  lebnumii  21989  phtpcer  22018  reparpht  22021  phtpcco2  22022  pcohtpy  22043  pcoass  22047  pcorevlem  22049  pi1cpbl  22067  pi1grplem  22072  isclmi  22100  cphsubrglem  22147  cphclm  22159  tchclm  22198  tchcph  22203  clsocv  22213  pjthlem2  22384  ovolf  22427  iundisj2  22494  vitalilem2  22559  vitali  22563  itg2monolem3  22702  dvfsumlem1  22970  dvfsumlem3  22972  mon1puc1p  23093  uc1pmon1p  23094  ply1remlem  23105  drnguc1p  23113  plyaddlem1  23159  coeidlem  23183  aannenlem2  23277  radcnvcl  23364  pilem2  23399  pilem2OLD  23400  coseq00topi  23449  coseq0negpitopi  23450  tangtx  23452  tanabsge  23453  cosq14gt0  23457  cosq14ge0  23458  cosordlem  23472  sinord  23475  resinf1o  23477  tanord1  23478  tanord  23479  efif1olem3  23485  efsubm  23492  relogrn  23503  logimclad  23514  logrnaddcl  23516  logneg  23529  logcj  23547  argregt0  23551  argrege0  23552  argimgt0  23553  argimlt0  23554  logimul  23555  logneg2  23556  logdmnrp  23578  logcnlem4  23582  dvloglem  23585  logf1o2  23587  efopnlem2  23594  cxpsqrtlem  23639  relogbval  23701  nnlogbexp  23710  relogbcxp  23714  relogbcxpb  23716  asinneg  23804  asinsin  23810  acoscos  23811  acosbnd  23818  atancj  23828  atanlogaddlem  23831  atanlogsublem  23833  atanlogsub  23834  atantan  23841  atanbndlem  23843  atans2  23849  leibpi  23860  scvxcvx  23903  jensenlem2  23905  emcllem7  23919  basellem1  23999  ppisval  24022  chtdif  24077  ppidif  24082  ppiub  24124  chtublem  24131  chtub  24132  lgsdilem2  24251  lgsquadlem1  24274  lgsquadlem2  24275  lgsquadlem3  24276  2sqlem3  24286  chebbnd1lem1  24299  chebbnd1lem2  24300  chebbnd1lem3  24301  dchrisumlem2  24320  dchrvmasumlem2  24328  dchrvmasumiflem1  24331  dchrisum0flblem2  24339  mulog2sumlem2  24365  logdivbnd  24386  pntpbnd2  24417  pntibndlem1  24419  pntibnd  24423  pntlemc  24425  pntlemg  24428  pntlemq  24431  pntlemf  24435  padicabvf  24461  padicabvcxp  24462  ostth2  24467  ttgcontlem1  24907  axpaschlem  24962  nbgraf1olem5  25165  cyclnspth  25351  wwlknred  25443  wwlknredwwlkn  25446  wwlkextproplem3  25463  clwlkisclwwlklem2fv1  25502  clwlkisclwwlklem2fv2  25503  clwlkisclwwlklem2a  25505  clwlkisclwwlklem1  25507  clwwlkel  25513  clwwlkf  25514  wwlkext2clwwlk  25523  clwwisshclwwlem1  25525  clwwisshclwwlem  25526  erclwwlkref  25533  usg2cwwkdifex  25541  clwlkfclwwlk1hash  25562  clwlkfclwwlk  25564  eupath2lem3  25699  extwwlkfablem2  25798  numclwlk2lem2f  25823  frgrareggt1  25836  grpoinvf  25960  strlem3a  27897  hstrlem3a  27905  iundisj2f  28196  fcoinver  28210  ssnnssfz  28367  bcm1n  28371  iundisj2fi  28373  fsumrp0cl  28459  submomnd  28474  lmodslmd  28521  suborng  28580  locfinreflem  28669  locfinref  28670  xrge0iifcnv  28741  xrge0iifiso  28743  xrge0iifhom  28745  esumc  28874  esumle  28881  esumlef  28885  esumpinfsum  28900  esumpcvgval  28901  fiunelros  28998  voliune  29054  volfiniune  29055  sibfinima  29174  eulerpartlemt  29206  fiblem  29233  fibp1  29236  dstrvprob  29306  ballotlemsel1i  29347  ballotlemfrceq  29363  ballotlemsel1iOLD  29385  ballotlemfrceqOLD  29401  eluzmn  29425  plymulx0  29438  signstfvc  29465  signstfveq0  29468  bnj944  29751  bnj998  29769  bnj1136  29808  bnj1408  29847  erdszelem4  29919  erdszelem8  29923  txsconlem  29965  cvxscon  29968  cvmliftpht  30043  snmlff  30054  elmrsubrn  30160  msrf  30182  mthmpps  30222  sinccvglem  30318  trer  30971  poimirlem6  31866  poimirlem7  31867  poimirlem9  31869  poimirlem17  31877  poimirlem20  31880  poimirlem28  31888  poimirlem29  31889  poimirlem30  31890  poimirlem31  31891  poimirlem32  31892  areacirc  31957  nnubfi  31999  prter1  32375  lkrlss  32586  diaf11N  34542  dibf11N  34654  lclkr  35026  lclkrs  35032  lcfrlem9  35043  lcfr  35078  mapd1o  35141  hdmapf1oN  35361  hgmapf1oN  35399  nacsfix  35479  eldioph2lem1  35527  irrapxlem1  35592  rmxypairf1o  35685  jm2.27a  35786  hbtlem2  35909  hbt  35915  cntzsdrg  35994  hashgcdlem  36000  mon1pid  36008  mon1psubm  36009  binomcxplemnotnn0  36569  elfzfzo  37334  monoords  37362  fmul01lt1lem2  37489  sumnnodd  37536  ioodvbdlimc1lem2  37630  ioodvbdlimc1lem2OLD  37632  ioodvbdlimc2lem  37634  ioodvbdlimc2lemOLD  37635  iblsplit  37669  iblspltprt  37676  itgspltprt  37682  stoweidlem11  37697  stoweidlem17  37703  fourierdlem12  37807  fourierdlem20  37815  fourierdlem25  37820  fourierdlem37  37833  fourierdlem41  37837  fourierdlem48  37844  fourierdlem49  37845  fourierdlem50  37846  fourierdlem54  37850  fourierdlem64  37860  fourierdlem73  37869  fourierdlem79  37875  fourierdlem102  37898  fourierdlem111  37907  fourierdlem114  37910  etransclem23  37948  etransclem48OLD  37973  etransclem48  37974  iccpartiltu  38454  iccpartigtl  38455  iccpartlt  38456  iccpartgt  38459  nnsum4primesevenALTV  38614  bgoldbtbndlem3  38620  lswn0  38638  pfxtrcfv0  38661  pfxeq  38663  pfxtrcfvl  38664  pfx2  38671  pfxccat3  38685  pfxccat3a  38688  2elfz2melfz  38753  elfzlble  38755  fzoopth  38758  structvtxvallem  38792  ringrng  39183  isringrng  39185  lidlrng  39231  ssnn0ssfz  39436  lmod1  39591  elfzolborelfzop1  39622  nn0o  39635  nnolog2flm1  39707
  Copyright terms: Public domain W3C validator