MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl3anbrc Structured version   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  4824  soisores  6039  onfununi  6595  smores2  6608  smoiso  6616  oelimcl  6835  iserd  6923  erinxp  6970  resixp  7089  undifixp  7090  alephval3  7981  fpwwe2lem12  8506  canthwelem  8515  canthwe  8516  r1limwun  8601  wunex2  8603  tskcard  8646  gruina  8683  nqerf  8797  nqerid  8800  uztrn  10492  zsupss  10555  xov1plusxeqvd  11031  elfzolt2b  11140  elfzolt3b  11141  elfzouz2  11143  fzossrbm1  11154  elfzo0  11161  fzostep1  11187  injresinjlem  11189  flword2  11210  uzsup  11234  fzsdom2  11683  ccatval1  11735  wrdeqs1cat  11779  swrds2  11870  rexuzre  12146  limsupgre  12265  rlimclim1  12329  rlimclim  12330  climrlim2  12331  isercolllem1  12448  isercoll  12451  climcndslem1  12619  tanhbnd  12752  sinbnd2  12773  cosbnd2  12774  rpnnen2  12815  bitsfzolem  12936  bitsfzo  12937  bitsmod  12938  bitsfi  12939  bitsinv1lem  12943  bitsinv1  12944  smueqlem  12992  zgz  13291  gznegcl  13293  gzcjcl  13294  gzaddcl  13295  gzmulcl  13296  vdwlem9  13347  ismred  13817  isfuncd  14052  homdmcoa  14212  isdrs2  14386  fpwipodrs  14580  ipodrsima  14581  psss  14636  psssdm2  14637  subgid  14936  issubg2  14949  subsubg  14953  gaorber  15075  orbsta  15080  pgpfi1  15219  subgpgp  15221  pgpssslw  15238  subgslw  15240  sylow2alem2  15242  fislw  15249  sylow3lem3  15253  efgs1  15357  efgsp1  15359  efgsres  15360  efgredleme  15365  efgcpbllemb  15377  lt6abl  15494  ablfac1eu  15621  isrngd  15688  prdsrngd  15708  subrgsubg  15864  islmodd  15946  islssd  16002  islss4  16028  gzrngunit  16754  zrngunit  16755  prmirredlem  16763  expmhm  16766  znidomb  16832  isphld  16875  ocvocv  16888  ocvlss  16889  2ndcctbss  17508  isfild  17880  infil  17885  neifil  17902  flimfcls  18048  istgp2  18111  oppgtmd  18117  oppgtgp  18118  distgp  18119  indistgp  18120  symgtgp  18121  submtmd  18124  subgtgp  18125  divstgplem  18140  prdstmdd  18143  prdstgpd  18144  tlmtgp  18215  isngp4  18648  subgngp  18666  ngptgp  18667  tngngp2  18683  nrgtrg  18715  nrgtdrg  18718  elii2  18951  icopnfcnv  18957  xrhmeo  18961  lebnumii  18981  phtpcer  19010  reparpht  19013  phtpcco2  19014  pcohtpy  19035  pcoass  19039  pcorevlem  19041  pi1cpbl  19059  pi1grplem  19064  isclmi  19092  cphsubrglem  19130  cphclm  19142  tchclm  19179  tchcph  19184  clsocv  19194  pjthlem2  19329  ovolf  19368  iundisj2  19433  vitalilem2  19491  vitali  19495  itg2monolem3  19634  dvfsumlem1  19900  dvfsumlem3  19902  mon1puc1p  20063  uc1pmon1p  20064  ply1remlem  20075  drnguc1p  20083  plyaddlem1  20122  coeidlem  20146  aannenlem2  20236  radcnvcl  20323  pilem2  20358  coseq00topi  20400  coseq0negpitopi  20401  tangtx  20403  tanabsge  20404  cosq14gt0  20408  cosq14ge0  20409  cosordlem  20423  sinord  20426  resinf1o  20428  tanord1  20429  tanord  20430  efif1olem3  20436  relogrn  20449  logimclad  20460  logrnaddcl  20462  logneg  20472  logcj  20491  argregt0  20495  argrege0  20496  argimgt0  20497  argimlt0  20498  logimul  20499  logneg2  20500  logdmnrp  20522  logcnlem4  20526  dvloglem  20529  logf1o2  20531  efopnlem2  20538  cxpsqrlem  20583  asinneg  20716  asinsin  20722  acoscos  20723  acosbnd  20730  atancj  20740  atanlogaddlem  20743  atanlogsublem  20745  atanlogsub  20746  atantan  20753  atanbndlem  20755  atans2  20761  leibpi  20772  scvxcvx  20814  jensenlem2  20816  emcllem7  20830  basellem1  20853  ppisval  20876  chtdif  20931  ppidif  20936  ppiub  20978  chtublem  20985  chtub  20986  lgsdilem2  21105  lgsquadlem1  21128  lgsquadlem2  21129  lgsquadlem3  21130  2sqlem3  21140  chebbnd1lem1  21153  chebbnd1lem2  21154  chebbnd1lem3  21155  dchrisumlem2  21174  dchrvmasumlem2  21182  dchrvmasumiflem1  21185  dchrisum0flblem2  21193  mulog2sumlem2  21219  logdivbnd  21240  pntpbnd2  21271  pntibndlem1  21273  pntibnd  21277  pntlemc  21279  pntlemg  21282  pntlemq  21285  pntlemf  21289  padicabvf  21315  padicabvcxp  21316  ostth2  21321  nbgraf1olem5  21445  cyclnspth  21608  cyclispthon  21610  eupath2lem3  21691  grpoinvf  21818  strlem3a  23745  hstrlem3a  23753  iundisj2f  24020  ssnnssfz  24138  bcm1n  24141  iundisj2fi  24143  fsumrp0cl  24207  subofld  24235  xrge0iifcnv  24309  xrge0iifiso  24311  xrge0iifhom  24313  rnlogbval  24390  nnlogbexp  24394  esumc  24436  esumle  24439  esumlef  24444  esumpinfsum  24457  esumpcvgval  24458  voliune  24575  volfiniune  24576  dstrvprob  24719  ballotlemsel1i  24760  ballotlemfrceq  24776  erdszelem4  24870  erdszelem8  24874  txsconlem  24917  cvxscon  24920  cvmliftpht  24995  snmlff  25006  sinccvglem  25099  fallfacval4  25349  axpaschlem  25844  areacirc  26251  trer  26273  finlocfin  26333  locfindis  26339  locfincf  26340  nnubfi  26408  prter1  26682  nacsfix  26720  eldioph2lem1  26772  irrapxlem1  26839  rmxypairf1o  26928  jm2.27a  27030  frlmlbs  27181  hbtlem2  27260  hbt  27266  pmtrfconj  27339  psgnunilem2  27350  psgnunilem3  27351  psgnunilem4  27352  cntzsdrg  27442  hashgcdlem  27448  mon1pid  27456  mon1psubm  27457  fmul01lt1lem2  27646  stoweidlem11  27691  stoweidlem17  27697  elfzelfzadd  28058  0elfz  28059  2elfz2melfz  28065  fzo0sn0fzo1  28072  ubmelfzo  28073  ubmelm1fzo  28074  elfzonelfzo  28079  ccatsymb  28116  swrd0swrd  28127  swrdswrd  28129  swrdccatin1  28135  swrdccatin12  28144  swrdccat3  28145  cshwidx  28172  2cshw1lem3  28180  2cshw2lem1  28182  lswrdn0  28190  cshw1  28202  cshwssizelem2  28208  cshwssizelem4a  28210  bnj944  29210  bnj998  29228  bnj1136  29267  bnj1408  29306  lkrlss  29794  diaf11N  31748  dibf11N  31860  lclkr  32232  lclkrs  32238  lcfrlem9  32249  lcfr  32284  mapd1o  32347  hdmapf1oN  32567  hgmapf1oN  32605
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