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

Theorem syl3anbrc 1167
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 1163 . 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 960
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 962
This theorem is referenced by:  soisores  6015  limuni3  6462  onfununi  6798  smores2  6811  smoiso  6819  oelimcl  7035  iserd  7123  erinxp  7170  resixp  7294  undifixp  7295  alephval3  8276  fpwwe2lem12  8804  canthwelem  8813  canthwe  8814  r1limwun  8899  wunex2  8901  tskcard  8944  gruina  8981  nqerf  9095  nqerid  9098  uzletr  10865  uztrn  10873  zsupss  10940  xov1plusxeqvd  11427  0elfz  11479  elfzelfzadd  11504  elfzolt2b  11559  elfzolt3b  11560  elfzouz2  11562  fzossrbm1  11574  elfzo0  11583  elfzodifsumelfzo  11600  fzonn0p1  11605  fzo0sn0fzo1  11613  ssfzo12bi  11618  ubmelm1fzo  11619  elfzonelfzo  11623  fzostep1  11631  injresinjlem  11634  flword2  11657  uzsup  11698  fzsdom2  12185  ccatval1  12272  swrdn0  12320  swrdtrcfv  12333  swrdtrcfv0  12334  swrdeq  12336  swrdsymbeq  12337  swrdtrcfvl  12340  swrdswrd  12350  swrdccatwrd  12358  wrdeqs1cat  12365  swrdccatin1  12370  swrdccat3  12379  swrdccatid  12384  repswswrd  12418  cshwidxmod  12436  cshw1  12452  swrds2  12541  2swrd2eqwrdeq  12549  rexuzre  12836  limsupgre  12955  rlimclim1  13019  rlimclim  13020  climrlim2  13021  isercolllem1  13138  isercoll  13141  climcndslem1  13308  tanhbnd  13441  sinbnd2  13462  cosbnd2  13463  rpnnen2  13504  bitsfzolem  13626  bitsfzo  13627  bitsmod  13628  bitsfi  13629  bitsinv1lem  13633  bitsinv1  13634  smueqlem  13682  zgz  13990  gznegcl  13992  gzcjcl  13993  gzaddcl  13994  gzmulcl  13995  vdwlem9  14046  cshwshashlem2  14119  ismred  14536  isfuncd  14771  homdmcoa  14931  isdrs2  15105  fpwipodrs  15330  ipodrsima  15331  psss  15380  psssdm2  15381  subgid  15676  issubg2  15689  subsubg  15697  gaorber  15819  orbsta  15824  pmtrfconj  15965  psgnunilem2  15994  psgnunilem3  15995  psgnunilem4  15996  pgpfi1  16087  subgpgp  16089  pgpssslw  16106  subgslw  16108  sylow2alem2  16110  fislw  16117  sylow3lem3  16121  efgs1  16225  efgsp1  16227  efgsres  16228  efgredleme  16233  efgcpbllemb  16245  lt6abl  16364  ablfac1eu  16564  isrngd  16669  prdsrngd  16694  subrgsubg  16851  islmodd  16934  islssd  16995  islss4  17021  gzrngunit  17837  expmhm  17839  zringunit  17873  zrngunit  17874  prmirredlem  17876  prmirredlemOLD  17879  znidomb  17953  isphld  18042  ocvocv  18055  ocvlss  18056  frlmlbs  18184  2ndcctbss  19018  isfild  19390  infil  19395  neifil  19412  flimfcls  19558  istgp2  19621  oppgtmd  19627  oppgtgp  19628  distgp  19629  indistgp  19630  symgtgp  19631  submtmd  19634  subgtgp  19635  divstgplem  19650  prdstmdd  19653  prdstgpd  19654  tlmtgp  19729  isngp4  20162  subgngp  20180  ngptgp  20181  tngngp2  20197  nrgtrg  20229  nrgtdrg  20232  elii2  20467  icopnfcnv  20473  xrhmeo  20477  lebnumii  20497  phtpcer  20526  reparpht  20529  phtpcco2  20530  pcohtpy  20551  pcoass  20555  pcorevlem  20557  pi1cpbl  20575  pi1grplem  20580  isclmi  20608  cphsubrglem  20655  cphclm  20667  tchclm  20706  tchcph  20711  clsocv  20721  pjthlem2  20884  ovolf  20924  iundisj2  20989  vitalilem2  21048  vitali  21052  itg2monolem3  21189  dvfsumlem1  21457  dvfsumlem3  21459  mon1puc1p  21581  uc1pmon1p  21582  ply1remlem  21593  drnguc1p  21601  plyaddlem1  21640  coeidlem  21664  aannenlem2  21754  radcnvcl  21841  pilem2  21876  coseq00topi  21923  coseq0negpitopi  21924  tangtx  21926  tanabsge  21927  cosq14gt0  21931  cosq14ge0  21932  cosordlem  21946  sinord  21949  resinf1o  21951  tanord1  21952  tanord  21953  efif1olem3  21959  relogrn  21972  logimclad  21983  logrnaddcl  21985  logneg  21995  logcj  22014  argregt0  22018  argrege0  22019  argimgt0  22020  argimlt0  22021  logimul  22022  logneg2  22023  logdmnrp  22045  logcnlem4  22049  dvloglem  22052  logf1o2  22054  efopnlem2  22061  cxpsqrlem  22106  asinneg  22240  asinsin  22246  acoscos  22247  acosbnd  22254  atancj  22264  atanlogaddlem  22267  atanlogsublem  22269  atanlogsub  22270  atantan  22277  atanbndlem  22279  atans2  22285  leibpi  22296  scvxcvx  22338  jensenlem2  22340  emcllem7  22354  basellem1  22377  ppisval  22400  chtdif  22455  ppidif  22460  ppiub  22502  chtublem  22509  chtub  22510  lgsdilem2  22629  lgsquadlem1  22652  lgsquadlem2  22653  lgsquadlem3  22654  2sqlem3  22664  chebbnd1lem1  22677  chebbnd1lem2  22678  chebbnd1lem3  22679  dchrisumlem2  22698  dchrvmasumlem2  22706  dchrvmasumiflem1  22709  dchrisum0flblem2  22717  mulog2sumlem2  22743  logdivbnd  22764  pntpbnd2  22795  pntibndlem1  22797  pntibnd  22801  pntlemc  22803  pntlemg  22806  pntlemq  22809  pntlemf  22813  padicabvf  22839  padicabvcxp  22840  ostth2  22845  ttgcontlem1  23066  axpaschlem  23121  nbgraf1olem5  23289  cyclnspth  23452  cyclispthon  23454  eupath2lem3  23535  grpoinvf  23662  strlem3a  25591  hstrlem3a  25599  iundisj2f  25867  ssnnssfz  26009  bcm1n  26012  iundisj2fi  26014  fsumrp0cl  26091  lmodslmd  26153  xrge0iifcnv  26299  xrge0iifiso  26301  xrge0iifhom  26303  rnlogbval  26395  nnlogbexp  26399  esumc  26441  esumle  26444  esumlef  26449  esumpinfsum  26462  esumpcvgval  26463  voliune  26581  volfiniune  26582  sibfinima  26655  eulerpartlemt  26684  dstrvprob  26784  ballotlemsel1i  26825  ballotlemfrceq  26841  plymulx0  26878  erdszelem4  27012  erdszelem8  27016  txsconlem  27059  cvxscon  27062  cvmliftpht  27137  snmlff  27148  sinccvglem  27246  fallfacval4  27475  areacirc  28414  trer  28436  finlocfin  28496  locfindis  28502  locfincf  28503  nnubfi  28571  prter1  28949  nacsfix  28973  eldioph2lem1  29023  irrapxlem1  29088  rmxypairf1o  29177  jm2.27a  29279  hbtlem2  29405  hbt  29411  cntzsdrg  29484  hashgcdlem  29490  mon1pid  29498  mon1psubm  29499  fmul01lt1lem2  29691  stoweidlem11  29731  stoweidlem17  29737  nn0ge2m1nn  30109  uzuzle  30115  nn0pzuz  30121  2elfz2melfz  30127  uzsubfz0  30130  ige2m1fz  30131  elfzlble  30133  el2fzo  30137  fzoopth  30138  elfzom1p1elfzo  30140  fzonn0p1p1  30141  elfzom1elfzo  30142  eluzgtdifelfzo  30144  fzosplitprm1  30149  prmn2uzge3  30174  lswn0  30183  ccatw2s1p1  30194  ccat2s1fvw  30196  wwlknred  30280  wwlknredwwlkn  30283  clwlkisclwwlklem2fv1  30369  clwlkisclwwlklem2fv2  30370  clwlkisclwwlklem2a  30372  clwlkisclwwlklem1  30374  clwwlkel  30380  clwwlkf  30381  wwlkext2clwwlk  30390  clwwisshclwwlem1  30394  clwwisshclwwlem  30395  erclwwlktr0  30404  erclwwlkref  30408  difelfzle  30412  difelfznle  30413  usg2cwwkdifex  30420  clwlkfclwwlk1hash  30440  clwlkfclwwlk  30442  wwlkextproplem3  30487  extwwlkfablem1  30592  extwwlkfablem2  30596  numclwlk2lem2f  30621  frgrareggt1  30634  lmod1  30875  bnj944  31765  bnj998  31783  bnj1136  31822  bnj1408  31861  lkrlss  32462  diaf11N  34416  dibf11N  34528  lclkr  34900  lclkrs  34906  lcfrlem9  34917  lcfr  34952  mapd1o  35015  hdmapf1oN  35235  hgmapf1oN  35273
  Copyright terms: Public domain W3C validator