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

Theorem syl3anbrc 1192
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 1188 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
5 syl3anbrc.4 . 2  |-  ( ta  <->  ( ps  /\  ch  /\  th ) )
64, 5sylibr 216 1  |-  ( ph  ->  ta )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    /\ w3a 985
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 189  df-an 373  df-3an 987
This theorem is referenced by:  soisores  6218  limuni3  6679  onfununi  7060  smores2  7073  smoiso  7081  oelimcl  7301  iserd  7389  erinxp  7437  resixp  7557  undifixp  7558  alephval3  8541  fpwwe2lem12  9066  canthwelem  9075  canthwe  9076  r1limwun  9161  wunex2  9163  tskcard  9206  gruina  9243  nqerf  9355  nqerid  9358  eluzuzle  11167  uztrn  11175  nn0pzuz  11216  zsupss  11253  nn0ge2m1nnALT  11258  xov1plusxeqvd  11778  ige2m1fz  11884  0elfz  11889  elfz0addOLD  11892  uzsubfz0  11898  elfzmlbm  11900  difelfzle  11904  difelfznle  11905  elfzolt2b  11931  elfzolt3b  11932  elfzouz2  11934  fzossrbm1  11947  elfzo0  11956  eluzgtdifelfzo  11976  elfzodifsumelfzo  11980  fzonn0p1  11990  fzonn0p1p1  11992  elfzom1p1elfzo  11993  fzo0sn0fzo1  12001  ssfzo12bi  12006  ubmelm1fzo  12007  elfzonelfzo  12011  fzosplitprm1  12018  fzostep1  12021  injresinjlem  12024  flword2  12048  uzsup  12090  fsuppmapnn0fiub  12203  suppssfz  12206  1elfz0hash  12569  fzsdom2  12600  ccatrn  12733  swrdn0  12786  swrdtrcfv  12797  swrdtrcfv0  12798  swrdeq  12800  swrdtrcfvl  12806  swrdswrd  12816  swrdccatwrd  12824  wrdeqs1cat  12831  swrdccatin1  12839  swrdccat3  12848  swrdccatid  12853  repswswrd  12887  cshwidxmod  12905  cshw1  12921  cshwcsh2id  12927  swrds2  13020  2swrd2eqwrdeq  13028  ccat2s1fvwALT  13030  rexuzre  13415  limsupgre  13542  limsupgreOLD  13543  rlimclim1  13609  rlimclim  13610  climrlim2  13611  isercolllem1  13728  isercoll  13731  climcndslem1  13907  fallfacval4  14096  tanhbnd  14215  sinbnd2  14236  cosbnd2  14237  rpnnen2  14278  bitsfzolem  14407  bitsfzolemOLD  14408  bitsfzo  14409  bitsmod  14410  bitsfi  14411  bitsinv1lem  14415  bitsinv1  14416  smueqlem  14464  prmn2uzge3  14644  zgz  14877  gznegcl  14879  gzcjcl  14880  gzaddcl  14881  gzmulcl  14882  vdwlem9  14939  prmgaplem3  15023  prmgaplem4  15024  cshwshashlem2  15067  ismred  15508  isfuncd  15770  homdmcoa  15962  isdrs2  16184  fpwipodrs  16410  ipodrsima  16411  psss  16460  psssdm2  16461  sgrp2rid2ex  16661  subgid  16819  issubg2  16832  subsubg  16840  gaorber  16962  orbsta  16967  pmtrfconj  17107  psgnunilem2  17136  psgnunilem3  17137  psgnunilem4  17138  pgpfi1  17247  subgpgp  17249  pgpssslw  17266  subgslw  17268  sylow2alem2  17270  fislw  17277  sylow3lem3  17281  efgs1  17385  efgsp1  17387  efgsres  17388  efgredleme  17393  efgcpbllemb  17405  lt6abl  17529  telgsumfzs  17619  ablfac1eu  17706  isringd  17815  ringsrg  17819  ring1  17830  prdsringd  17840  subrgsubg  18014  islmodd  18097  islssd  18159  islss4  18185  gsummoncoe1  18898  gzrngunit  19033  expmhm  19036  zringunit  19062  prmirredlem  19064  znidomb  19132  isphld  19221  ocvocv  19234  ocvlss  19235  frlmlbs  19355  mp2pm2mplem4  19833  chfacfisf  19878  chfacfisfcpmat  19879  chfacfscmulfsupp  19883  chfacfpmmulfsupp  19887  chfacfpmmulgsum2  19889  2ndcctbss  20470  finlocfin  20535  dissnlocfin  20544  locfindis  20545  locfincf  20546  isfild  20873  infil  20878  neifil  20895  flimfcls  21041  istgp2  21106  oppgtmd  21112  oppgtgp  21113  distgp  21114  indistgp  21115  symgtgp  21116  submtmd  21119  subgtgp  21120  qustgplem  21135  prdstmdd  21138  prdstgpd  21139  tlmtgp  21210  isngp4  21625  subgngp  21643  ngptgp  21644  tngngp2  21660  nrgtrg  21692  nrgtdrg  21695  elii2  21964  icopnfcnv  21970  xrhmeo  21974  lebnumii  21997  phtpcer  22026  reparpht  22029  phtpcco2  22030  pcohtpy  22051  pcoass  22055  pcorevlem  22057  pi1cpbl  22075  pi1grplem  22080  isclmi  22108  cphsubrglem  22155  cphclm  22167  tchclm  22206  tchcph  22211  clsocv  22221  pjthlem2  22392  ovolf  22435  iundisj2  22502  vitalilem2  22567  vitali  22571  itg2monolem3  22710  dvfsumlem1  22978  dvfsumlem3  22980  mon1puc1p  23101  uc1pmon1p  23102  ply1remlem  23113  drnguc1p  23121  plyaddlem1  23167  coeidlem  23191  aannenlem2  23285  radcnvcl  23372  pilem2  23407  pilem2OLD  23408  coseq00topi  23457  coseq0negpitopi  23458  tangtx  23460  tanabsge  23461  cosq14gt0  23465  cosq14ge0  23466  cosordlem  23480  sinord  23483  resinf1o  23485  tanord1  23486  tanord  23487  efif1olem3  23493  efsubm  23500  relogrn  23511  logimclad  23522  logrnaddcl  23524  logneg  23537  logcj  23555  argregt0  23559  argrege0  23560  argimgt0  23561  argimlt0  23562  logimul  23563  logneg2  23564  logdmnrp  23586  logcnlem4  23590  dvloglem  23593  logf1o2  23595  efopnlem2  23602  cxpsqrtlem  23647  relogbval  23709  nnlogbexp  23718  relogbcxp  23722  relogbcxpb  23724  asinneg  23812  asinsin  23818  acoscos  23819  acosbnd  23826  atancj  23836  atanlogaddlem  23839  atanlogsublem  23841  atanlogsub  23842  atantan  23849  atanbndlem  23851  atans2  23857  leibpi  23868  scvxcvx  23911  jensenlem2  23913  emcllem7  23927  basellem1  24007  ppisval  24030  chtdif  24085  ppidif  24090  ppiub  24132  chtublem  24139  chtub  24140  lgsdilem2  24259  lgsquadlem1  24282  lgsquadlem2  24283  lgsquadlem3  24284  2sqlem3  24294  chebbnd1lem1  24307  chebbnd1lem2  24308  chebbnd1lem3  24309  dchrisumlem2  24328  dchrvmasumlem2  24336  dchrvmasumiflem1  24339  dchrisum0flblem2  24347  mulog2sumlem2  24373  logdivbnd  24394  pntpbnd2  24425  pntibndlem1  24427  pntibnd  24431  pntlemc  24433  pntlemg  24436  pntlemq  24439  pntlemf  24443  padicabvf  24469  padicabvcxp  24470  ostth2  24475  ttgcontlem1  24915  axpaschlem  24970  nbgraf1olem5  25173  cyclnspth  25359  wwlknred  25451  wwlknredwwlkn  25454  wwlkextproplem3  25471  clwlkisclwwlklem2fv1  25510  clwlkisclwwlklem2fv2  25511  clwlkisclwwlklem2a  25513  clwlkisclwwlklem1  25515  clwwlkel  25521  clwwlkf  25522  wwlkext2clwwlk  25531  clwwisshclwwlem1  25533  clwwisshclwwlem  25534  erclwwlkref  25541  usg2cwwkdifex  25549  clwlkfclwwlk1hash  25570  clwlkfclwwlk  25572  eupath2lem3  25707  extwwlkfablem2  25806  numclwlk2lem2f  25831  frgrareggt1  25844  grpoinvf  25968  strlem3a  27905  hstrlem3a  27913  iundisj2f  28200  fcoinver  28214  ssnnssfz  28367  bcm1n  28371  iundisj2fi  28373  fsumrp0cl  28458  submomnd  28473  lmodslmd  28520  suborng  28578  locfinreflem  28667  locfinref  28668  xrge0iifcnv  28739  xrge0iifiso  28741  xrge0iifhom  28743  esumc  28872  esumle  28879  esumlef  28883  esumpinfsum  28898  esumpcvgval  28899  fiunelros  28996  voliune  29052  volfiniune  29053  sibfinima  29172  eulerpartlemt  29204  fiblem  29231  fibp1  29234  dstrvprob  29304  ballotlemsel1i  29345  ballotlemfrceq  29361  ballotlemsel1iOLD  29383  ballotlemfrceqOLD  29399  eluzmn  29423  plymulx0  29436  signstfvc  29463  signstfveq0  29466  bnj944  29749  bnj998  29767  bnj1136  29806  bnj1408  29845  erdszelem4  29917  erdszelem8  29921  txsconlem  29963  cvxscon  29966  cvmliftpht  30041  snmlff  30052  elmrsubrn  30158  msrf  30180  mthmpps  30220  sinccvglem  30316  trer  30972  poimirlem6  31946  poimirlem7  31947  poimirlem9  31949  poimirlem17  31957  poimirlem20  31960  poimirlem28  31968  poimirlem29  31969  poimirlem30  31970  poimirlem31  31971  poimirlem32  31972  areacirc  32037  nnubfi  32079  prter1  32451  lkrlss  32661  diaf11N  34617  dibf11N  34729  lclkr  35101  lclkrs  35107  lcfrlem9  35118  lcfr  35153  mapd1o  35216  hdmapf1oN  35436  hgmapf1oN  35474  nacsfix  35554  eldioph2lem1  35602  irrapxlem1  35666  rmxypairf1o  35759  jm2.27a  35860  hbtlem2  35983  hbt  35989  cntzsdrg  36068  hashgcdlem  36074  mon1pid  36082  mon1psubm  36083  binomcxplemnotnn0  36705  elfzfzo  37486  monoords  37514  fmul01lt1lem2  37663  sumnnodd  37710  ioodvbdlimc1lem2  37804  ioodvbdlimc1lem2OLD  37806  ioodvbdlimc2lem  37808  ioodvbdlimc2lemOLD  37809  iblsplit  37843  iblspltprt  37850  itgspltprt  37856  stoweidlem11  37871  stoweidlem17  37877  fourierdlem12  37981  fourierdlem20  37989  fourierdlem25  37994  fourierdlem37  38007  fourierdlem41  38011  fourierdlem48  38018  fourierdlem49  38019  fourierdlem50  38020  fourierdlem54  38024  fourierdlem64  38034  fourierdlem73  38043  fourierdlem79  38049  fourierdlem102  38072  fourierdlem111  38081  fourierdlem114  38084  etransclem23  38122  etransclem48OLD  38147  etransclem48  38148  iccpartiltu  38736  iccpartigtl  38737  iccpartlt  38738  iccpartgt  38741  nnsum4primesevenALTV  38896  bgoldbtbndlem3  38902  lswn0  38920  pfxtrcfv0  38943  pfxeq  38945  pfxtrcfvl  38946  pfx2  38953  pfxccat3  38967  pfxccat3a  38970  2elfz2melfz  39058  elfzlble  39060  fzoopth  39063  structvtxvallem  39122  ringrng  39932  isringrng  39934  lidlrng  39980  ssnn0ssfz  40183  lmod1  40338  elfzolborelfzop1  40369  nn0o  40382  nnolog2flm1  40454
  Copyright terms: Public domain W3C validator