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

Theorem syl3anbrc 1138
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 1134 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
5 syl3anbrc.4 . 2  |-  ( ta  <->  ( ps  /\  ch  /\  th ) )
64, 5sylibr 204 1  |-  ( ph  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ w3a 936
This theorem is referenced by:  limuni3  4791  soisores  6006  onfununi  6562  smores2  6575  smoiso  6583  oelimcl  6802  iserd  6890  erinxp  6937  resixp  7056  undifixp  7057  alephval3  7947  fpwwe2lem12  8472  canthwelem  8481  canthwe  8482  r1limwun  8567  wunex2  8569  tskcard  8612  gruina  8649  nqerf  8763  nqerid  8766  uztrn  10458  zsupss  10521  xov1plusxeqvd  10997  elfzolt2b  11105  elfzolt3b  11106  elfzouz2  11108  fzossrbm1  11119  elfzo0  11126  fzostep1  11152  injresinjlem  11154  flword2  11175  uzsup  11199  fzsdom2  11648  ccatval1  11700  wrdeqs1cat  11744  swrds2  11835  rexuzre  12111  limsupgre  12230  rlimclim1  12294  rlimclim  12295  climrlim2  12296  isercolllem1  12413  isercoll  12416  climcndslem1  12584  tanhbnd  12717  sinbnd2  12738  cosbnd2  12739  rpnnen2  12780  bitsfzolem  12901  bitsfzo  12902  bitsmod  12903  bitsfi  12904  bitsinv1lem  12908  bitsinv1  12909  smueqlem  12957  zgz  13256  gznegcl  13258  gzcjcl  13259  gzaddcl  13260  gzmulcl  13261  vdwlem9  13312  ismred  13782  isfuncd  14017  homdmcoa  14177  isdrs2  14351  fpwipodrs  14545  ipodrsima  14546  psss  14601  psssdm2  14602  subgid  14901  issubg2  14914  subsubg  14918  gaorber  15040  orbsta  15045  pgpfi1  15184  subgpgp  15186  pgpssslw  15203  subgslw  15205  sylow2alem2  15207  fislw  15214  sylow3lem3  15218  efgs1  15322  efgsp1  15324  efgsres  15325  efgredleme  15330  efgcpbllemb  15342  lt6abl  15459  ablfac1eu  15586  isrngd  15653  prdsrngd  15673  subrgsubg  15829  islmodd  15911  islssd  15967  islss4  15993  gzrngunit  16719  zrngunit  16720  prmirredlem  16728  expmhm  16731  znidomb  16797  isphld  16840  ocvocv  16853  ocvlss  16854  2ndcctbss  17471  isfild  17843  infil  17848  neifil  17865  flimfcls  18011  istgp2  18074  oppgtmd  18080  oppgtgp  18081  distgp  18082  indistgp  18083  symgtgp  18084  submtmd  18087  subgtgp  18088  divstgplem  18103  prdstmdd  18106  prdstgpd  18107  tlmtgp  18178  isngp4  18611  subgngp  18629  ngptgp  18630  tngngp2  18646  nrgtrg  18678  nrgtdrg  18681  elii2  18914  icopnfcnv  18920  xrhmeo  18924  lebnumii  18944  phtpcer  18973  reparpht  18976  phtpcco2  18977  pcohtpy  18998  pcoass  19002  pcorevlem  19004  pi1cpbl  19022  pi1grplem  19027  isclmi  19055  cphsubrglem  19093  cphclm  19105  tchclm  19142  tchcph  19147  clsocv  19157  pjthlem2  19292  ovolf  19331  iundisj2  19396  vitalilem2  19454  vitali  19458  itg2monolem3  19597  dvfsumlem1  19863  dvfsumlem3  19865  mon1puc1p  20026  uc1pmon1p  20027  ply1remlem  20038  drnguc1p  20046  plyaddlem1  20085  coeidlem  20109  aannenlem2  20199  radcnvcl  20286  pilem2  20321  coseq00topi  20363  coseq0negpitopi  20364  tangtx  20366  tanabsge  20367  cosq14gt0  20371  cosq14ge0  20372  cosordlem  20386  sinord  20389  resinf1o  20391  tanord1  20392  tanord  20393  efif1olem3  20399  relogrn  20412  logimclad  20423  logrnaddcl  20425  logneg  20435  logcj  20454  argregt0  20458  argrege0  20459  argimgt0  20460  argimlt0  20461  logimul  20462  logneg2  20463  logdmnrp  20485  logcnlem4  20489  dvloglem  20492  logf1o2  20494  efopnlem2  20501  cxpsqrlem  20546  asinneg  20679  asinsin  20685  acoscos  20686  acosbnd  20693  atancj  20703  atanlogaddlem  20706  atanlogsublem  20708  atanlogsub  20709  atantan  20716  atanbndlem  20718  atans2  20724  leibpi  20735  scvxcvx  20777  jensenlem2  20779  emcllem7  20793  basellem1  20816  ppisval  20839  chtdif  20894  ppidif  20899  ppiub  20941  chtublem  20948  chtub  20949  lgsdilem2  21068  lgsquadlem1  21091  lgsquadlem2  21092  lgsquadlem3  21093  2sqlem3  21103  chebbnd1lem1  21116  chebbnd1lem2  21117  chebbnd1lem3  21118  dchrisumlem2  21137  dchrvmasumlem2  21145  dchrvmasumiflem1  21148  dchrisum0flblem2  21156  mulog2sumlem2  21182  logdivbnd  21203  pntpbnd2  21234  pntibndlem1  21236  pntibnd  21240  pntlemc  21242  pntlemg  21245  pntlemq  21248  pntlemf  21252  padicabvf  21278  padicabvcxp  21279  ostth2  21284  nbgraf1olem5  21408  cyclnspth  21571  cyclispthon  21573  eupath2lem3  21654  grpoinvf  21781  strlem3a  23708  hstrlem3a  23716  iundisj2f  23983  ssnnssfz  24101  bcm1n  24104  iundisj2fi  24106  fsumrp0cl  24170  subofld  24198  xrge0iifcnv  24272  xrge0iifiso  24274  xrge0iifhom  24276  rnlogbval  24353  nnlogbexp  24357  esumc  24399  esumle  24402  esumlef  24407  esumpinfsum  24420  esumpcvgval  24421  voliune  24538  volfiniune  24539  dstrvprob  24682  ballotlemsel1i  24723  ballotlemfrceq  24739  erdszelem4  24833  erdszelem8  24837  txsconlem  24880  cvxscon  24883  cvmliftpht  24958  snmlff  24969  sinccvglem  25062  axpaschlem  25783  areacirc  26187  trer  26209  finlocfin  26269  locfindis  26275  locfincf  26276  nnubfi  26344  prter1  26618  nacsfix  26656  eldioph2lem1  26708  irrapxlem1  26775  rmxypairf1o  26864  jm2.27a  26966  frlmlbs  27117  hbtlem2  27196  hbt  27202  pmtrfconj  27275  psgnunilem2  27286  psgnunilem3  27287  psgnunilem4  27288  cntzsdrg  27378  hashgcdlem  27384  mon1pid  27392  mon1psubm  27393  fmul01lt1lem2  27582  stoweidlem11  27627  stoweidlem17  27633  elfzelfzadd  27982  0elfz  27983  ubmelfzo  27986  ubmelm1fzo  27987  elfzonelfzo  27992  swrd0swrd  28009  swrdswrd  28011  swrdccatin1  28016  swrdccatin12  28026  swrdccatin12b  28027  swrdccat3  28029  bnj944  29015  bnj998  29033  bnj1136  29072  bnj1408  29111  lkrlss  29578  diaf11N  31532  dibf11N  31644  lclkr  32016  lclkrs  32022  lcfrlem9  32033  lcfr  32068  mapd1o  32131  hdmapf1oN  32351  hgmapf1oN  32389
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator