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

Theorem syl3anbrc 1180
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 1176 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
5 syl3anbrc.4 . 2  |-  ( ta  <->  ( ps  /\  ch  /\  th ) )
64, 5sylibr 212 1  |-  ( ph  ->  ta )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ w3a 973
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 185  df-an 371  df-3an 975
This theorem is referenced by:  soisores  6209  limuni3  6665  onfununi  7009  smores2  7022  smoiso  7030  oelimcl  7246  iserd  7334  erinxp  7382  resixp  7501  undifixp  7502  alephval3  8487  fpwwe2lem12  9015  canthwelem  9024  canthwe  9025  r1limwun  9110  wunex2  9112  tskcard  9155  gruina  9192  nqerf  9304  nqerid  9307  eluzuzle  11086  uztrn  11094  nn0pzuz  11134  zsupss  11167  nn0ge2m1nnALT  11172  xov1plusxeqvd  11662  ige2m1fz  11763  0elfz  11768  elfz0add  11770  uzsubfz0  11776  difelfzle  11781  difelfznle  11782  elfzolt2b  11803  elfzolt3b  11804  elfzouz2  11806  fzossrbm1  11818  elfzo0  11827  eluzgtdifelfzo  11842  elfzodifsumelfzo  11846  fzonn0p1  11856  fzonn0p1p1  11858  elfzom1p1elfzo  11859  fzo0sn0fzo1  11866  ssfzo12bi  11871  ubmelm1fzo  11872  elfzonelfzo  11876  fzosplitprm1  11883  fzostep1  11886  injresinjlem  11889  flword2  11912  uzsup  11953  fsuppmapnn0fiub  12060  suppssfz  12063  fzsdom2  12445  ccatval1  12554  ccatw2s1p1  12597  swrdn0  12612  swrdtrcfv  12625  swrdtrcfv0  12626  swrdeq  12628  swrdsymbeq  12629  swrdtrcfvl  12632  swrdswrd  12642  swrdccatwrd  12650  wrdeqs1cat  12657  swrdccatin1  12665  swrdccat3  12674  swrdccatid  12679  repswswrd  12713  cshwidxmod  12731  cshw1  12747  cshwcsh2id  12753  swrds2  12840  2swrd2eqwrdeq  12848  ccat2s1fvwALT  12850  rexuzre  13141  limsupgre  13260  rlimclim1  13324  rlimclim  13325  climrlim2  13326  isercolllem1  13443  isercoll  13446  climcndslem1  13617  tanhbnd  13750  sinbnd2  13771  cosbnd2  13772  rpnnen2  13813  bitsfzolem  13936  bitsfzo  13937  bitsmod  13938  bitsfi  13939  bitsinv1lem  13943  bitsinv1  13944  smueqlem  13992  prmn2uzge3  14089  zgz  14303  gznegcl  14305  gzcjcl  14306  gzaddcl  14307  gzmulcl  14308  vdwlem9  14359  cshwshashlem2  14432  ismred  14850  isfuncd  15085  homdmcoa  15245  isdrs2  15419  fpwipodrs  15644  ipodrsima  15645  psss  15694  psssdm2  15695  subgid  15995  issubg2  16008  subsubg  16016  gaorber  16138  orbsta  16143  pmtrfconj  16284  psgnunilem2  16313  psgnunilem3  16314  psgnunilem4  16315  pgpfi1  16408  subgpgp  16410  pgpssslw  16427  subgslw  16429  sylow2alem2  16431  fislw  16438  sylow3lem3  16442  efgs1  16546  efgsp1  16548  efgsres  16549  efgredleme  16554  efgcpbllemb  16566  lt6abl  16685  telgsumfzs  16806  ablfac1eu  16911  isrngd  17017  prdsrngd  17042  subrgsubg  17215  islmodd  17298  islssd  17362  islss4  17388  gsummoncoe1  18114  gzrngunit  18248  expmhm  18250  zringunit  18284  zrngunit  18285  prmirredlem  18287  prmirredlemOLD  18290  znidomb  18364  isphld  18453  ocvocv  18466  ocvlss  18467  frlmlbs  18595  mp2pm2mplem4  19074  chfacfisf  19119  chfacfisfcpmat  19120  chfacfscmulfsupp  19124  chfacfpmmulfsupp  19128  chfacfpmmulgsum2  19130  2ndcctbss  19719  isfild  20091  infil  20096  neifil  20113  flimfcls  20259  istgp2  20322  oppgtmd  20328  oppgtgp  20329  distgp  20330  indistgp  20331  symgtgp  20332  submtmd  20335  subgtgp  20336  divstgplem  20351  prdstmdd  20354  prdstgpd  20355  tlmtgp  20430  isngp4  20863  subgngp  20881  ngptgp  20882  tngngp2  20898  nrgtrg  20930  nrgtdrg  20933  elii2  21168  icopnfcnv  21174  xrhmeo  21178  lebnumii  21198  phtpcer  21227  reparpht  21230  phtpcco2  21231  pcohtpy  21252  pcoass  21256  pcorevlem  21258  pi1cpbl  21276  pi1grplem  21281  isclmi  21309  cphsubrglem  21356  cphclm  21368  tchclm  21407  tchcph  21412  clsocv  21422  pjthlem2  21585  ovolf  21625  iundisj2  21691  vitalilem2  21750  vitali  21754  itg2monolem3  21891  dvfsumlem1  22159  dvfsumlem3  22161  mon1puc1p  22283  uc1pmon1p  22284  ply1remlem  22295  drnguc1p  22303  plyaddlem1  22342  coeidlem  22366  aannenlem2  22456  radcnvcl  22543  pilem2  22578  coseq00topi  22625  coseq0negpitopi  22626  tangtx  22628  tanabsge  22629  cosq14gt0  22633  cosq14ge0  22634  cosordlem  22648  sinord  22651  resinf1o  22653  tanord1  22654  tanord  22655  efif1olem3  22661  relogrn  22674  logimclad  22685  logrnaddcl  22687  logneg  22697  logcj  22716  argregt0  22720  argrege0  22721  argimgt0  22722  argimlt0  22723  logimul  22724  logneg2  22725  logdmnrp  22747  logcnlem4  22751  dvloglem  22754  logf1o2  22756  efopnlem2  22763  cxpsqrtlem  22808  asinneg  22942  asinsin  22948  acoscos  22949  acosbnd  22956  atancj  22966  atanlogaddlem  22969  atanlogsublem  22971  atanlogsub  22972  atantan  22979  atanbndlem  22981  atans2  22987  leibpi  22998  scvxcvx  23040  jensenlem2  23042  emcllem7  23056  basellem1  23079  ppisval  23102  chtdif  23157  ppidif  23162  ppiub  23204  chtublem  23211  chtub  23212  lgsdilem2  23331  lgsquadlem1  23354  lgsquadlem2  23355  lgsquadlem3  23356  2sqlem3  23366  chebbnd1lem1  23379  chebbnd1lem2  23380  chebbnd1lem3  23381  dchrisumlem2  23400  dchrvmasumlem2  23408  dchrvmasumiflem1  23411  dchrisum0flblem2  23419  mulog2sumlem2  23445  logdivbnd  23466  pntpbnd2  23497  pntibndlem1  23499  pntibnd  23503  pntlemc  23505  pntlemg  23508  pntlemq  23511  pntlemf  23515  padicabvf  23541  padicabvcxp  23542  ostth2  23547  ttgcontlem1  23861  axpaschlem  23916  nbgraf1olem5  24118  cyclnspth  24304  cyclispthon  24306  wwlknred  24396  wwlknredwwlkn  24399  wwlkextproplem3  24416  clwlkisclwwlklem2fv1  24455  clwlkisclwwlklem2fv2  24456  clwlkisclwwlklem2a  24458  clwlkisclwwlklem1  24460  clwwlkel  24466  clwwlkf  24467  wwlkext2clwwlk  24476  clwwisshclwwlem1  24478  clwwisshclwwlem  24479  erclwwlkref  24486  usg2cwwkdifex  24494  clwlkfclwwlk1hash  24515  clwlkfclwwlk  24517  eupath2lem3  24652  extwwlkfablem1  24748  extwwlkfablem2  24752  numclwlk2lem2f  24777  frgrareggt1  24790  grpoinvf  24915  strlem3a  26844  hstrlem3a  26852  iundisj2f  27119  ssnnssfz  27262  bcm1n  27265  iundisj2fi  27267  fsumrp0cl  27344  lmodslmd  27406  xrge0iifcnv  27548  xrge0iifiso  27550  xrge0iifhom  27552  rnlogbval  27653  nnlogbexp  27657  esumc  27699  esumle  27702  esumlef  27707  esumpinfsum  27720  esumpcvgval  27721  voliune  27838  volfiniune  27839  sibfinima  27918  eulerpartlemt  27947  dstrvprob  28047  ballotlemsel1i  28088  ballotlemfrceq  28104  plymulx0  28141  erdszelem4  28275  erdszelem8  28279  txsconlem  28322  cvxscon  28325  cvmliftpht  28400  snmlff  28411  sinccvglem  28510  fallfacval4  28739  areacirc  29687  trer  29709  finlocfin  29769  locfindis  29775  locfincf  29776  nnubfi  29844  prter1  30222  nacsfix  30246  eldioph2lem1  30295  irrapxlem1  30360  rmxypairf1o  30449  jm2.27a  30551  hbtlem2  30677  hbt  30683  cntzsdrg  30756  hashgcdlem  30762  mon1pid  30770  mon1psubm  30771  elfzfzo  31035  fmul01lt1lem2  31135  itgspltprt  31297  stoweidlem11  31311  stoweidlem17  31317  fourierdlem12  31419  fourierdlem20  31427  fourierdlem73  31480  2elfz2melfz  31803  elfzlble  31805  el2fzo  31808  fzoopth  31809  lswn0  31812  ringrng0  31982  ssnn0ssfz  32002  lmod1  32174  bnj944  33075  bnj998  33093  bnj1136  33132  bnj1408  33171  lkrlss  33892  diaf11N  35846  dibf11N  35958  lclkr  36330  lclkrs  36336  lcfrlem9  36347  lcfr  36382  mapd1o  36445  hdmapf1oN  36665  hgmapf1oN  36703
  Copyright terms: Public domain W3C validator