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

Theorem syl3anbrc 1172
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 1168 . 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 965
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 967
This theorem is referenced by:  soisores  6030  limuni3  6475  onfununi  6814  smores2  6827  smoiso  6835  oelimcl  7051  iserd  7139  erinxp  7186  resixp  7310  undifixp  7311  alephval3  8292  fpwwe2lem12  8820  canthwelem  8829  canthwe  8830  r1limwun  8915  wunex2  8917  tskcard  8960  gruina  8997  nqerf  9111  nqerid  9114  uzletr  10881  uztrn  10889  zsupss  10956  xov1plusxeqvd  11443  0elfz  11495  elfzelfzadd  11520  elfzolt2b  11575  elfzolt3b  11576  elfzouz2  11578  fzossrbm1  11590  elfzo0  11599  elfzodifsumelfzo  11616  fzonn0p1  11621  fzo0sn0fzo1  11629  ssfzo12bi  11634  ubmelm1fzo  11635  elfzonelfzo  11639  fzostep1  11647  injresinjlem  11650  flword2  11673  uzsup  11714  fzsdom2  12201  ccatval1  12288  swrdn0  12336  swrdtrcfv  12349  swrdtrcfv0  12350  swrdeq  12352  swrdsymbeq  12353  swrdtrcfvl  12356  swrdswrd  12366  swrdccatwrd  12374  wrdeqs1cat  12381  swrdccatin1  12386  swrdccat3  12395  swrdccatid  12400  repswswrd  12434  cshwidxmod  12452  cshw1  12468  swrds2  12557  2swrd2eqwrdeq  12565  rexuzre  12852  limsupgre  12971  rlimclim1  13035  rlimclim  13036  climrlim2  13037  isercolllem1  13154  isercoll  13157  climcndslem1  13324  tanhbnd  13457  sinbnd2  13478  cosbnd2  13479  rpnnen2  13520  bitsfzolem  13642  bitsfzo  13643  bitsmod  13644  bitsfi  13645  bitsinv1lem  13649  bitsinv1  13650  smueqlem  13698  zgz  14006  gznegcl  14008  gzcjcl  14009  gzaddcl  14010  gzmulcl  14011  vdwlem9  14062  cshwshashlem2  14135  ismred  14552  isfuncd  14787  homdmcoa  14947  isdrs2  15121  fpwipodrs  15346  ipodrsima  15347  psss  15396  psssdm2  15397  subgid  15695  issubg2  15708  subsubg  15716  gaorber  15838  orbsta  15843  pmtrfconj  15984  psgnunilem2  16013  psgnunilem3  16014  psgnunilem4  16015  pgpfi1  16106  subgpgp  16108  pgpssslw  16125  subgslw  16127  sylow2alem2  16129  fislw  16136  sylow3lem3  16140  efgs1  16244  efgsp1  16246  efgsres  16247  efgredleme  16252  efgcpbllemb  16264  lt6abl  16383  ablfac1eu  16586  isrngd  16691  prdsrngd  16716  subrgsubg  16883  islmodd  16966  islssd  17029  islss4  17055  gzrngunit  17890  expmhm  17892  zringunit  17926  zrngunit  17927  prmirredlem  17929  prmirredlemOLD  17932  znidomb  18006  isphld  18095  ocvocv  18108  ocvlss  18109  frlmlbs  18237  2ndcctbss  19071  isfild  19443  infil  19448  neifil  19465  flimfcls  19611  istgp2  19674  oppgtmd  19680  oppgtgp  19681  distgp  19682  indistgp  19683  symgtgp  19684  submtmd  19687  subgtgp  19688  divstgplem  19703  prdstmdd  19706  prdstgpd  19707  tlmtgp  19782  isngp4  20215  subgngp  20233  ngptgp  20234  tngngp2  20250  nrgtrg  20282  nrgtdrg  20285  elii2  20520  icopnfcnv  20526  xrhmeo  20530  lebnumii  20550  phtpcer  20579  reparpht  20582  phtpcco2  20583  pcohtpy  20604  pcoass  20608  pcorevlem  20610  pi1cpbl  20628  pi1grplem  20633  isclmi  20661  cphsubrglem  20708  cphclm  20720  tchclm  20759  tchcph  20764  clsocv  20774  pjthlem2  20937  ovolf  20977  iundisj2  21042  vitalilem2  21101  vitali  21105  itg2monolem3  21242  dvfsumlem1  21510  dvfsumlem3  21512  mon1puc1p  21634  uc1pmon1p  21635  ply1remlem  21646  drnguc1p  21654  plyaddlem1  21693  coeidlem  21717  aannenlem2  21807  radcnvcl  21894  pilem2  21929  coseq00topi  21976  coseq0negpitopi  21977  tangtx  21979  tanabsge  21980  cosq14gt0  21984  cosq14ge0  21985  cosordlem  21999  sinord  22002  resinf1o  22004  tanord1  22005  tanord  22006  efif1olem3  22012  relogrn  22025  logimclad  22036  logrnaddcl  22038  logneg  22048  logcj  22067  argregt0  22071  argrege0  22072  argimgt0  22073  argimlt0  22074  logimul  22075  logneg2  22076  logdmnrp  22098  logcnlem4  22102  dvloglem  22105  logf1o2  22107  efopnlem2  22114  cxpsqrlem  22159  asinneg  22293  asinsin  22299  acoscos  22300  acosbnd  22307  atancj  22317  atanlogaddlem  22320  atanlogsublem  22322  atanlogsub  22323  atantan  22330  atanbndlem  22332  atans2  22338  leibpi  22349  scvxcvx  22391  jensenlem2  22393  emcllem7  22407  basellem1  22430  ppisval  22453  chtdif  22508  ppidif  22513  ppiub  22555  chtublem  22562  chtub  22563  lgsdilem2  22682  lgsquadlem1  22705  lgsquadlem2  22706  lgsquadlem3  22707  2sqlem3  22717  chebbnd1lem1  22730  chebbnd1lem2  22731  chebbnd1lem3  22732  dchrisumlem2  22751  dchrvmasumlem2  22759  dchrvmasumiflem1  22762  dchrisum0flblem2  22770  mulog2sumlem2  22796  logdivbnd  22817  pntpbnd2  22848  pntibndlem1  22850  pntibnd  22854  pntlemc  22856  pntlemg  22859  pntlemq  22862  pntlemf  22866  padicabvf  22892  padicabvcxp  22893  ostth2  22898  ttgcontlem1  23143  axpaschlem  23198  nbgraf1olem5  23366  cyclnspth  23529  cyclispthon  23531  eupath2lem3  23612  grpoinvf  23739  strlem3a  25668  hstrlem3a  25676  iundisj2f  25944  ssnnssfz  26088  bcm1n  26091  iundisj2fi  26093  fsumrp0cl  26170  lmodslmd  26232  xrge0iifcnv  26375  xrge0iifiso  26377  xrge0iifhom  26379  rnlogbval  26471  nnlogbexp  26475  esumc  26517  esumle  26520  esumlef  26525  esumpinfsum  26538  esumpcvgval  26539  voliune  26657  volfiniune  26658  sibfinima  26737  eulerpartlemt  26766  dstrvprob  26866  ballotlemsel1i  26907  ballotlemfrceq  26923  plymulx0  26960  erdszelem4  27094  erdszelem8  27098  txsconlem  27141  cvxscon  27144  cvmliftpht  27219  snmlff  27230  sinccvglem  27329  fallfacval4  27558  areacirc  28501  trer  28523  finlocfin  28583  locfindis  28589  locfincf  28590  nnubfi  28658  prter1  29036  nacsfix  29060  eldioph2lem1  29110  irrapxlem1  29175  rmxypairf1o  29264  jm2.27a  29366  hbtlem2  29492  hbt  29498  cntzsdrg  29571  hashgcdlem  29577  mon1pid  29585  mon1psubm  29586  fmul01lt1lem2  29778  stoweidlem11  29818  stoweidlem17  29824  nn0ge2m1nn  30196  uzuzle  30202  nn0pzuz  30208  2elfz2melfz  30214  uzsubfz0  30217  ige2m1fz  30218  elfzlble  30220  el2fzo  30224  fzoopth  30225  elfzom1p1elfzo  30227  fzonn0p1p1  30228  elfzom1elfzo  30229  eluzgtdifelfzo  30231  fzosplitprm1  30236  prmn2uzge3  30261  lswn0  30270  ccatw2s1p1  30281  ccat2s1fvw  30283  wwlknred  30367  wwlknredwwlkn  30370  clwlkisclwwlklem2fv1  30456  clwlkisclwwlklem2fv2  30457  clwlkisclwwlklem2a  30459  clwlkisclwwlklem1  30461  clwwlkel  30467  clwwlkf  30468  wwlkext2clwwlk  30477  clwwisshclwwlem1  30481  clwwisshclwwlem  30482  erclwwlktr0  30491  erclwwlkref  30495  difelfzle  30499  difelfznle  30500  usg2cwwkdifex  30507  clwlkfclwwlk1hash  30527  clwlkfclwwlk  30529  wwlkextproplem3  30574  extwwlkfablem1  30679  extwwlkfablem2  30683  numclwlk2lem2f  30708  frgrareggt1  30721  ssnn0ssfz  30753  suppssfz  30798  fsuppmapnn0fiub  30811  telescfzgsumlem  30821  gsummoncoe1  30855  mp2pm2mplem4  30931  lmod1  31046  bnj944  31943  bnj998  31961  bnj1136  32000  bnj1408  32039  lkrlss  32752  diaf11N  34706  dibf11N  34818  lclkr  35190  lclkrs  35196  lcfrlem9  35207  lcfr  35242  mapd1o  35305  hdmapf1oN  35525  hgmapf1oN  35563
  Copyright terms: Public domain W3C validator