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  4772  soisores  5986  onfununi  6539  smores2  6552  smoiso  6560  oelimcl  6779  iserd  6867  erinxp  6914  resixp  7033  undifixp  7034  alephval3  7924  fpwwe2lem12  8449  canthwelem  8458  canthwe  8459  r1limwun  8544  wunex2  8546  tskcard  8589  gruina  8626  nqerf  8740  nqerid  8743  uztrn  10434  zsupss  10497  xov1plusxeqvd  10973  elfzolt2b  11080  elfzolt3b  11081  elfzouz2  11083  fzossrbm1  11094  elfzo0  11101  fzostep1  11124  injresinjlem  11126  flword2  11147  uzsup  11171  fzsdom2  11620  ccatval1  11672  wrdeqs1cat  11716  swrds2  11807  rexuzre  12083  limsupgre  12202  rlimclim1  12266  rlimclim  12267  climrlim2  12268  isercolllem1  12385  isercoll  12388  climcndslem1  12556  tanhbnd  12689  sinbnd2  12710  cosbnd2  12711  rpnnen2  12752  bitsfzolem  12873  bitsfzo  12874  bitsmod  12875  bitsfi  12876  bitsinv1lem  12880  bitsinv1  12881  smueqlem  12929  zgz  13228  gznegcl  13230  gzcjcl  13231  gzaddcl  13232  gzmulcl  13233  vdwlem9  13284  ismred  13754  isfuncd  13989  homdmcoa  14149  isdrs2  14323  fpwipodrs  14517  ipodrsima  14518  psss  14573  psssdm2  14574  subgid  14873  issubg2  14886  subsubg  14890  gaorber  15012  orbsta  15017  pgpfi1  15156  subgpgp  15158  pgpssslw  15175  subgslw  15177  sylow2alem2  15179  fislw  15186  sylow3lem3  15190  efgs1  15294  efgsp1  15296  efgsres  15297  efgredleme  15302  efgcpbllemb  15314  lt6abl  15431  ablfac1eu  15558  isrngd  15625  prdsrngd  15645  subrgsubg  15801  islmodd  15883  islssd  15939  islss4  15965  gzrngunit  16687  zrngunit  16688  prmirredlem  16696  expmhm  16699  znidomb  16765  isphld  16808  ocvocv  16821  ocvlss  16822  2ndcctbss  17439  isfild  17811  infil  17816  neifil  17833  flimfcls  17979  istgp2  18042  oppgtmd  18048  oppgtgp  18049  distgp  18050  indistgp  18051  symgtgp  18052  submtmd  18055  subgtgp  18056  divstgplem  18071  prdstmdd  18074  prdstgpd  18075  tlmtgp  18146  isngp4  18529  subgngp  18547  ngptgp  18548  tngngp2  18564  nrgtrg  18596  nrgtdrg  18599  elii2  18832  icopnfcnv  18838  xrhmeo  18842  lebnumii  18862  phtpcer  18891  reparpht  18894  phtpcco2  18895  pcohtpy  18916  pcoass  18920  pcorevlem  18922  pi1cpbl  18940  pi1grplem  18945  isclmi  18973  cphsubrglem  19011  cphclm  19023  tchclm  19060  tchcph  19065  clsocv  19075  pjthlem2  19206  ovolf  19245  iundisj2  19310  vitalilem2  19368  vitali  19372  itg2monolem3  19511  dvfsumlem1  19777  dvfsumlem3  19779  mon1puc1p  19940  uc1pmon1p  19941  ply1remlem  19952  drnguc1p  19960  plyaddlem1  19999  coeidlem  20023  aannenlem2  20113  radcnvcl  20200  pilem2  20235  coseq00topi  20277  coseq0negpitopi  20278  tangtx  20280  tanabsge  20281  cosq14gt0  20285  cosq14ge0  20286  cosordlem  20300  sinord  20303  resinf1o  20305  tanord1  20306  tanord  20307  efif1olem3  20313  relogrn  20326  logimclad  20337  logrnaddcl  20339  logneg  20349  logcj  20368  argregt0  20372  argrege0  20373  argimgt0  20374  argimlt0  20375  logimul  20376  logneg2  20377  logdmnrp  20399  logcnlem4  20403  dvloglem  20406  logf1o2  20408  efopnlem2  20415  cxpsqrlem  20460  asinneg  20593  asinsin  20599  acoscos  20600  acosbnd  20607  atancj  20617  atanlogaddlem  20620  atanlogsublem  20622  atanlogsub  20623  atantan  20630  atanbndlem  20632  atans2  20638  leibpi  20649  scvxcvx  20691  jensenlem2  20693  emcllem7  20707  basellem1  20730  ppisval  20753  chtdif  20808  ppidif  20813  ppiub  20855  chtublem  20862  chtub  20863  lgsdilem2  20982  lgsquadlem1  21005  lgsquadlem2  21006  lgsquadlem3  21007  2sqlem3  21017  chebbnd1lem1  21030  chebbnd1lem2  21031  chebbnd1lem3  21032  dchrisumlem2  21051  dchrvmasumlem2  21059  dchrvmasumiflem1  21062  dchrisum0flblem2  21070  mulog2sumlem2  21096  logdivbnd  21117  pntpbnd2  21148  pntibndlem1  21150  pntibnd  21154  pntlemc  21156  pntlemg  21159  pntlemq  21162  pntlemf  21166  padicabvf  21192  padicabvcxp  21193  ostth2  21198  nbgraf1olem5  21321  cyclnspth  21466  cyclispthon  21468  eupath2lem3  21549  grpoinvf  21676  strlem3a  23603  hstrlem3a  23611  iundisj2f  23873  ssnnssfz  23984  bcm1n  23987  iundisj2fi  23991  fsumrp0cl  24046  subofld  24071  xrge0iifcnv  24123  xrge0iifiso  24125  xrge0iifhom  24127  rnlogbval  24196  nnlogbexp  24200  esumc  24242  esumle  24245  esumlef  24250  esumpinfsum  24263  esumpcvgval  24264  voliune  24379  volfiniune  24380  dstrvprob  24508  ballotlemsel1i  24549  ballotlemfrceq  24565  erdszelem4  24659  erdszelem8  24663  txsconlem  24706  cvxscon  24709  cvmliftpht  24784  snmlff  24795  sinccvglem  24888  axpaschlem  25593  areacirc  25988  trer  26010  finlocfin  26070  locfindis  26076  locfincf  26077  nnubfi  26145  prter1  26419  nacsfix  26457  eldioph2lem1  26509  irrapxlem1  26576  rmxypairf1o  26665  jm2.27a  26767  frlmlbs  26918  hbtlem2  26997  hbt  27003  pmtrfconj  27076  psgnunilem2  27087  psgnunilem3  27088  psgnunilem4  27089  cntzsdrg  27179  hashgcdlem  27185  mon1pid  27193  mon1psubm  27194  fmul01lt1lem2  27383  stoweidlem11  27428  stoweidlem17  27434  bnj944  28647  bnj998  28665  bnj1136  28704  bnj1408  28743  lkrlss  29210  diaf11N  31164  dibf11N  31276  lclkr  31648  lclkrs  31654  lcfrlem9  31665  lcfr  31700  mapd1o  31763  hdmapf1oN  31983  hgmapf1oN  32021
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