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

Theorem syl3anbrc 1181
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 1177 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
5 syl3anbrc.4 . 2  |-  ( ta  <->  ( ps  /\  ch  /\  th ) )
64, 5sylibr 212 1  |-  ( ph  ->  ta )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ w3a 974
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 185  df-an 371  df-3an 976
This theorem is referenced by:  soisores  6208  limuni3  6672  onfununi  7014  smores2  7027  smoiso  7035  oelimcl  7251  iserd  7339  erinxp  7387  resixp  7506  undifixp  7507  alephval3  8494  fpwwe2lem12  9022  canthwelem  9031  canthwe  9032  r1limwun  9117  wunex2  9119  tskcard  9162  gruina  9199  nqerf  9311  nqerid  9314  eluzuzle  11100  uztrn  11108  nn0pzuz  11149  zsupss  11182  nn0ge2m1nnALT  11187  xov1plusxeqvd  11677  ige2m1fz  11779  0elfz  11784  elfz0addOLD  11787  uzsubfz0  11793  elfzmlbm  11795  difelfzle  11799  difelfznle  11800  elfzolt2b  11821  elfzolt3b  11822  elfzouz2  11824  fzossrbm1  11836  elfzo0  11845  eluzgtdifelfzo  11860  elfzodifsumelfzo  11864  fzonn0p1  11874  fzonn0p1p1  11876  elfzom1p1elfzo  11877  fzo0sn0fzo1  11884  ssfzo12bi  11889  ubmelm1fzo  11890  elfzonelfzo  11894  fzosplitprm1  11901  fzostep1  11904  injresinjlem  11907  flword2  11931  uzsup  11972  fsuppmapnn0fiub  12079  suppssfz  12082  fzsdom2  12468  ccatval1  12577  ccatrn  12588  ccatw2s1p1  12622  swrdn0  12637  swrdtrcfv  12650  swrdtrcfv0  12651  swrdeq  12653  swrdsymbeq  12654  swrdtrcfvl  12657  swrdswrd  12667  swrdccatwrd  12675  wrdeqs1cat  12682  swrdccatin1  12690  swrdccat3  12699  swrdccatid  12704  repswswrd  12738  cshwidxmod  12756  cshw1  12772  cshwcsh2id  12778  swrds2  12865  2swrd2eqwrdeq  12873  ccat2s1fvwALT  12875  rexuzre  13167  limsupgre  13286  rlimclim1  13350  rlimclim  13351  climrlim2  13352  isercolllem1  13469  isercoll  13472  climcndslem1  13643  tanhbnd  13878  sinbnd2  13899  cosbnd2  13900  rpnnen2  13941  bitsfzolem  14066  bitsfzo  14067  bitsmod  14068  bitsfi  14069  bitsinv1lem  14073  bitsinv1  14074  smueqlem  14122  prmn2uzge3  14219  zgz  14433  gznegcl  14435  gzcjcl  14436  gzaddcl  14437  gzmulcl  14438  vdwlem9  14489  cshwshashlem2  14563  ismred  14981  isfuncd  15213  homdmcoa  15373  isdrs2  15547  fpwipodrs  15773  ipodrsima  15774  psss  15823  psssdm2  15824  sgrp2rid2ex  16024  subgid  16182  issubg2  16195  subsubg  16203  gaorber  16325  orbsta  16330  pmtrfconj  16470  psgnunilem2  16499  psgnunilem3  16500  psgnunilem4  16501  pgpfi1  16594  subgpgp  16596  pgpssslw  16613  subgslw  16615  sylow2alem2  16617  fislw  16624  sylow3lem3  16628  efgs1  16732  efgsp1  16734  efgsres  16735  efgredleme  16740  efgcpbllemb  16752  lt6abl  16876  telgsumfzs  16997  ablfac1eu  17103  isringd  17212  ringsrg  17216  ring1  17227  prdsringd  17240  subrgsubg  17414  islmodd  17497  islssd  17561  islss4  17587  gsummoncoe1  18325  gzrngunit  18462  expmhm  18464  zringunit  18498  zrngunit  18499  prmirredlem  18501  prmirredlemOLD  18504  znidomb  18578  isphld  18667  ocvocv  18680  ocvlss  18681  frlmlbs  18809  mp2pm2mplem4  19288  chfacfisf  19333  chfacfisfcpmat  19334  chfacfscmulfsupp  19338  chfacfpmmulfsupp  19342  chfacfpmmulgsum2  19344  2ndcctbss  19934  finlocfin  19999  dissnlocfin  20008  locfindis  20009  locfincf  20010  isfild  20337  infil  20342  neifil  20359  flimfcls  20505  istgp2  20568  oppgtmd  20574  oppgtgp  20575  distgp  20576  indistgp  20577  symgtgp  20578  submtmd  20581  subgtgp  20582  qustgplem  20597  prdstmdd  20600  prdstgpd  20601  tlmtgp  20676  isngp4  21109  subgngp  21127  ngptgp  21128  tngngp2  21144  nrgtrg  21176  nrgtdrg  21179  elii2  21414  icopnfcnv  21420  xrhmeo  21424  lebnumii  21444  phtpcer  21473  reparpht  21476  phtpcco2  21477  pcohtpy  21498  pcoass  21502  pcorevlem  21504  pi1cpbl  21522  pi1grplem  21527  isclmi  21555  cphsubrglem  21602  cphclm  21614  tchclm  21653  tchcph  21658  clsocv  21668  pjthlem2  21831  ovolf  21871  iundisj2  21937  vitalilem2  21996  vitali  22000  itg2monolem3  22137  dvfsumlem1  22405  dvfsumlem3  22407  mon1puc1p  22529  uc1pmon1p  22530  ply1remlem  22541  drnguc1p  22549  plyaddlem1  22588  coeidlem  22612  aannenlem2  22703  radcnvcl  22790  pilem2  22825  coseq00topi  22873  coseq0negpitopi  22874  tangtx  22876  tanabsge  22877  cosq14gt0  22881  cosq14ge0  22882  cosordlem  22896  sinord  22899  resinf1o  22901  tanord1  22902  tanord  22903  efif1olem3  22909  efsubm  22916  relogrn  22927  logimclad  22938  logrnaddcl  22940  logneg  22950  logcj  22969  argregt0  22973  argrege0  22974  argimgt0  22975  argimlt0  22976  logimul  22977  logneg2  22978  logdmnrp  23000  logcnlem4  23004  dvloglem  23007  logf1o2  23009  efopnlem2  23016  cxpsqrtlem  23061  asinneg  23195  asinsin  23201  acoscos  23202  acosbnd  23209  atancj  23219  atanlogaddlem  23222  atanlogsublem  23224  atanlogsub  23225  atantan  23232  atanbndlem  23234  atans2  23240  leibpi  23251  scvxcvx  23293  jensenlem2  23295  emcllem7  23309  basellem1  23332  ppisval  23355  chtdif  23410  ppidif  23415  ppiub  23457  chtublem  23464  chtub  23465  lgsdilem2  23584  lgsquadlem1  23607  lgsquadlem2  23608  lgsquadlem3  23609  2sqlem3  23619  chebbnd1lem1  23632  chebbnd1lem2  23633  chebbnd1lem3  23634  dchrisumlem2  23653  dchrvmasumlem2  23661  dchrvmasumiflem1  23664  dchrisum0flblem2  23672  mulog2sumlem2  23698  logdivbnd  23719  pntpbnd2  23750  pntibndlem1  23752  pntibnd  23756  pntlemc  23758  pntlemg  23761  pntlemq  23764  pntlemf  23768  padicabvf  23794  padicabvcxp  23795  ostth2  23800  ttgcontlem1  24166  axpaschlem  24221  nbgraf1olem5  24423  cyclnspth  24609  wwlknred  24701  wwlknredwwlkn  24704  wwlkextproplem3  24721  clwlkisclwwlklem2fv1  24760  clwlkisclwwlklem2fv2  24761  clwlkisclwwlklem2a  24763  clwlkisclwwlklem1  24765  clwwlkel  24771  clwwlkf  24772  wwlkext2clwwlk  24781  clwwisshclwwlem1  24783  clwwisshclwwlem  24784  erclwwlkref  24791  usg2cwwkdifex  24799  clwlkfclwwlk1hash  24820  clwlkfclwwlk  24822  eupath2lem3  24957  extwwlkfablem2  25056  numclwlk2lem2f  25081  frgrareggt1  25094  grpoinvf  25220  strlem3a  27149  hstrlem3a  27157  iundisj2f  27427  fcoinver  27438  ssnnssfz  27575  bcm1n  27578  iundisj2fi  27580  fsumrp0cl  27663  submomnd  27678  lmodslmd  27725  suborng  27783  locfinreflem  27821  locfinref  27822  xrge0iifcnv  27893  xrge0iifiso  27895  xrge0iifhom  27897  rnlogbval  27994  nnlogbexp  27998  esumc  28040  esumle  28043  esumlef  28048  esumpinfsum  28061  esumpcvgval  28062  voliune  28179  volfiniune  28180  sibfinima  28259  eulerpartlemt  28288  fiblem  28315  fibp1  28318  dstrvprob  28388  ballotlemsel1i  28429  ballotlemfrceq  28445  eluzmn  28469  plymulx0  28482  signstfvc  28509  signstfveq0  28512  erdszelem4  28616  erdszelem8  28620  txsconlem  28663  cvxscon  28666  cvmliftpht  28741  snmlff  28752  elmrsubrn  28858  msrf  28880  mthmpps  28920  sinccvglem  29016  fallfacval4  29141  areacirc  30088  trer  30110  nnubfi  30219  prter1  30596  nacsfix  30620  eldioph2lem1  30669  irrapxlem1  30734  rmxypairf1o  30823  jm2.27a  30923  hbtlem2  31049  hbt  31055  cntzsdrg  31127  hashgcdlem  31133  mon1pid  31141  mon1psubm  31142  elfzfzo  31412  monoords  31450  fmul01lt1lem2  31533  sumnnodd  31590  ioodvbdlimc1lem2  31683  ioodvbdlimc2lem  31685  iblsplit  31719  iblspltprt  31726  itgspltprt  31732  stoweidlem11  31747  stoweidlem17  31753  fourierdlem12  31855  fourierdlem20  31863  fourierdlem25  31868  fourierdlem37  31880  fourierdlem41  31884  fourierdlem48  31891  fourierdlem49  31892  fourierdlem50  31893  fourierdlem54  31897  fourierdlem64  31907  fourierdlem73  31916  fourierdlem79  31922  fourierdlem102  31945  fourierdlem111  31954  fourierdlem114  31957  2elfz2melfz  32288  elfzlble  32290  el2fzo  32293  fzoopth  32294  lswn0  32297  ringrng  32523  isringrng  32525  lidlrng  32560  ssnn0ssfz  32806  lmod1  32963  bnj944  33864  bnj998  33882  bnj1136  33921  bnj1408  33960  lkrlss  34695  diaf11N  36651  dibf11N  36763  lclkr  37135  lclkrs  37141  lcfrlem9  37152  lcfr  37187  mapd1o  37250  hdmapf1oN  37470  hgmapf1oN  37508
  Copyright terms: Public domain W3C validator