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

Theorem syl3anbrc 1183
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 1179 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
5 syl3anbrc.4 . 2  |-  ( ta  <->  ( ps  /\  ch  /\  th ) )
64, 5sylibr 214 1  |-  ( ph  ->  ta )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 186    /\ w3a 976
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 187  df-an 371  df-3an 978
This theorem is referenced by:  soisores  6208  limuni3  6672  onfununi  7047  smores2  7060  smoiso  7068  oelimcl  7288  iserd  7376  erinxp  7424  resixp  7544  undifixp  7545  alephval3  8525  fpwwe2lem12  9051  canthwelem  9060  canthwe  9061  r1limwun  9146  wunex2  9148  tskcard  9191  gruina  9228  nqerf  9340  nqerid  9343  eluzuzle  11137  uztrn  11145  nn0pzuz  11186  zsupss  11218  nn0ge2m1nnALT  11223  xov1plusxeqvd  11722  ige2m1fz  11825  0elfz  11830  elfz0addOLD  11833  uzsubfz0  11839  elfzmlbm  11841  difelfzle  11845  difelfznle  11846  elfzolt2b  11872  elfzolt3b  11873  elfzouz2  11875  fzossrbm1  11888  elfzo0  11897  eluzgtdifelfzo  11916  elfzodifsumelfzo  11920  fzonn0p1  11930  fzonn0p1p1  11932  elfzom1p1elfzo  11933  fzo0sn0fzo1  11941  ssfzo12bi  11946  ubmelm1fzo  11947  elfzonelfzo  11951  fzosplitprm1  11958  fzostep1  11961  injresinjlem  11964  flword2  11988  uzsup  12030  fsuppmapnn0fiub  12143  suppssfz  12146  1elfz0hash  12508  fzsdom2  12537  ccatrn  12662  swrdn0  12713  swrdtrcfv  12724  swrdtrcfv0  12725  swrdeq  12727  swrdtrcfvl  12733  swrdswrd  12743  swrdccatwrd  12751  wrdeqs1cat  12758  swrdccatin1  12766  swrdccat3  12775  swrdccatid  12780  repswswrd  12814  cshwidxmod  12832  cshw1  12848  cshwcsh2id  12854  swrds2  12941  2swrd2eqwrdeq  12949  ccat2s1fvwALT  12951  rexuzre  13336  limsupgre  13455  rlimclim1  13519  rlimclim  13520  climrlim2  13521  isercolllem1  13638  isercoll  13641  climcndslem1  13814  fallfacval4  13990  tanhbnd  14107  sinbnd2  14128  cosbnd2  14129  rpnnen2  14170  bitsfzolem  14295  bitsfzo  14296  bitsmod  14297  bitsfi  14298  bitsinv1lem  14302  bitsinv1  14303  smueqlem  14351  prmn2uzge3  14448  zgz  14662  gznegcl  14664  gzcjcl  14665  gzaddcl  14666  gzmulcl  14667  vdwlem9  14718  cshwshashlem2  14792  ismred  15218  isfuncd  15480  homdmcoa  15672  isdrs2  15894  fpwipodrs  16120  ipodrsima  16121  psss  16170  psssdm2  16171  sgrp2rid2ex  16371  subgid  16529  issubg2  16542  subsubg  16550  gaorber  16672  orbsta  16677  pmtrfconj  16817  psgnunilem2  16846  psgnunilem3  16847  psgnunilem4  16848  pgpfi1  16941  subgpgp  16943  pgpssslw  16960  subgslw  16962  sylow2alem2  16964  fislw  16971  sylow3lem3  16975  efgs1  17079  efgsp1  17081  efgsres  17082  efgredleme  17087  efgcpbllemb  17099  lt6abl  17223  telgsumfzs  17340  ablfac1eu  17446  isringd  17555  ringsrg  17559  ring1  17570  prdsringd  17583  subrgsubg  17757  islmodd  17840  islssd  17904  islss4  17930  gsummoncoe1  18668  gzrngunit  18805  expmhm  18807  zringunit  18830  prmirredlem  18832  znidomb  18900  isphld  18989  ocvocv  19002  ocvlss  19003  frlmlbs  19126  mp2pm2mplem4  19604  chfacfisf  19649  chfacfisfcpmat  19650  chfacfscmulfsupp  19654  chfacfpmmulfsupp  19658  chfacfpmmulgsum2  19660  2ndcctbss  20250  finlocfin  20315  dissnlocfin  20324  locfindis  20325  locfincf  20326  isfild  20653  infil  20658  neifil  20675  flimfcls  20821  istgp2  20884  oppgtmd  20890  oppgtgp  20891  distgp  20892  indistgp  20893  symgtgp  20894  submtmd  20897  subgtgp  20898  qustgplem  20913  prdstmdd  20916  prdstgpd  20917  tlmtgp  20992  isngp4  21425  subgngp  21443  ngptgp  21444  tngngp2  21460  nrgtrg  21492  nrgtdrg  21495  elii2  21730  icopnfcnv  21736  xrhmeo  21740  lebnumii  21760  phtpcer  21789  reparpht  21792  phtpcco2  21793  pcohtpy  21814  pcoass  21818  pcorevlem  21820  pi1cpbl  21838  pi1grplem  21843  isclmi  21871  cphsubrglem  21918  cphclm  21930  tchclm  21969  tchcph  21974  clsocv  21984  pjthlem2  22147  ovolf  22187  iundisj2  22253  vitalilem2  22312  vitali  22316  itg2monolem3  22453  dvfsumlem1  22721  dvfsumlem3  22723  mon1puc1p  22845  uc1pmon1p  22846  ply1remlem  22857  drnguc1p  22865  plyaddlem1  22904  coeidlem  22928  aannenlem2  23019  radcnvcl  23106  pilem2  23141  coseq00topi  23189  coseq0negpitopi  23190  tangtx  23192  tanabsge  23193  cosq14gt0  23197  cosq14ge0  23198  cosordlem  23212  sinord  23215  resinf1o  23217  tanord1  23218  tanord  23219  efif1olem3  23225  efsubm  23232  relogrn  23243  logimclad  23254  logrnaddcl  23256  logneg  23269  logcj  23287  argregt0  23291  argrege0  23292  argimgt0  23293  argimlt0  23294  logimul  23295  logneg2  23296  logdmnrp  23318  logcnlem4  23322  dvloglem  23325  logf1o2  23327  efopnlem2  23334  cxpsqrtlem  23379  relogbval  23441  nnlogbexp  23450  relogbcxp  23454  relogbcxpb  23456  asinneg  23544  asinsin  23550  acoscos  23551  acosbnd  23558  atancj  23568  atanlogaddlem  23571  atanlogsublem  23573  atanlogsub  23574  atantan  23581  atanbndlem  23583  atans2  23589  leibpi  23600  scvxcvx  23643  jensenlem2  23645  emcllem7  23659  basellem1  23737  ppisval  23760  chtdif  23815  ppidif  23820  ppiub  23862  chtublem  23869  chtub  23870  lgsdilem2  23989  lgsquadlem1  24012  lgsquadlem2  24013  lgsquadlem3  24014  2sqlem3  24024  chebbnd1lem1  24037  chebbnd1lem2  24038  chebbnd1lem3  24039  dchrisumlem2  24058  dchrvmasumlem2  24066  dchrvmasumiflem1  24069  dchrisum0flblem2  24077  mulog2sumlem2  24103  logdivbnd  24124  pntpbnd2  24155  pntibndlem1  24157  pntibnd  24161  pntlemc  24163  pntlemg  24166  pntlemq  24169  pntlemf  24173  padicabvf  24199  padicabvcxp  24200  ostth2  24205  ttgcontlem1  24617  axpaschlem  24672  nbgraf1olem5  24874  cyclnspth  25060  wwlknred  25152  wwlknredwwlkn  25155  wwlkextproplem3  25172  clwlkisclwwlklem2fv1  25211  clwlkisclwwlklem2fv2  25212  clwlkisclwwlklem2a  25214  clwlkisclwwlklem1  25216  clwwlkel  25222  clwwlkf  25223  wwlkext2clwwlk  25232  clwwisshclwwlem1  25234  clwwisshclwwlem  25235  erclwwlkref  25242  usg2cwwkdifex  25250  clwlkfclwwlk1hash  25271  clwlkfclwwlk  25273  eupath2lem3  25408  extwwlkfablem2  25507  numclwlk2lem2f  25532  frgrareggt1  25545  grpoinvf  25669  strlem3a  27597  hstrlem3a  27605  iundisj2f  27895  fcoinver  27909  ssnnssfz  28058  bcm1n  28061  iundisj2fi  28063  fsumrp0cl  28150  submomnd  28165  lmodslmd  28212  suborng  28271  locfinreflem  28309  locfinref  28310  xrge0iifcnv  28381  xrge0iifiso  28383  xrge0iifhom  28385  esumc  28511  esumle  28518  esumlef  28522  esumpinfsum  28537  esumpcvgval  28538  fiunelros  28635  voliune  28691  volfiniune  28692  sibfinima  28800  eulerpartlemt  28829  fiblem  28856  fibp1  28859  dstrvprob  28929  ballotlemsel1i  28970  ballotlemfrceq  28986  eluzmn  29010  plymulx0  29023  signstfvc  29050  signstfveq0  29053  bnj944  29336  bnj998  29354  bnj1136  29393  bnj1408  29432  erdszelem4  29504  erdszelem8  29508  txsconlem  29550  cvxscon  29553  cvmliftpht  29628  snmlff  29639  elmrsubrn  29745  msrf  29767  mthmpps  29807  sinccvglem  29903  trer  30557  areacirc  31496  nnubfi  31538  prter1  31915  lkrlss  32126  diaf11N  34082  dibf11N  34194  lclkr  34566  lclkrs  34572  lcfrlem9  34583  lcfr  34618  mapd1o  34681  hdmapf1oN  34901  hgmapf1oN  34939  nacsfix  35019  eldioph2lem1  35067  irrapxlem1  35132  rmxypairf1o  35221  jm2.27a  35322  hbtlem2  35450  hbt  35456  cntzsdrg  35528  hashgcdlem  35534  mon1pid  35542  mon1psubm  35543  binomcxplemnotnn0  36122  elfzfzo  36845  monoords  36878  fmul01lt1lem2  36960  sumnnodd  37017  ioodvbdlimc1lem2  37110  ioodvbdlimc2lem  37112  iblsplit  37146  iblspltprt  37153  itgspltprt  37159  stoweidlem11  37174  stoweidlem17  37180  fourierdlem12  37282  fourierdlem20  37290  fourierdlem25  37295  fourierdlem37  37307  fourierdlem41  37311  fourierdlem48  37318  fourierdlem49  37319  fourierdlem50  37320  fourierdlem54  37324  fourierdlem64  37334  fourierdlem73  37343  fourierdlem79  37349  fourierdlem102  37372  fourierdlem111  37381  fourierdlem114  37384  etransclem23  37421  etransclem48  37446  iccpartiltu  37702  iccpartigtl  37703  iccpartlt  37704  iccpartgt  37707  nnsum4primesevenALTV  37862  bgoldbtbndlem3  37868  lswn0  37879  pfxtrcfv0  37902  pfxeq  37904  pfxtrcfvl  37905  pfx2  37912  pfxccat3  37926  pfxccat3a  37929  2elfz2melfz  37979  elfzlble  37981  fzoopth  37984  ringrng  38209  isringrng  38211  lidlrng  38257  ssnn0ssfz  38462  lmod1  38617  elfzolborelfzop1  38649  nn0o  38662  nnolog2flm1  38734
  Copyright terms: Public domain W3C validator