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

Theorem syl3anbrc 1244
Description: Syllogism inference. (Contributed by Mario Carneiro, 11-May-2014.)
Hypotheses
Ref Expression
syl3anbrc.1 (𝜑𝜓)
syl3anbrc.2 (𝜑𝜒)
syl3anbrc.3 (𝜑𝜃)
syl3anbrc.4 (𝜏 ↔ (𝜓𝜒𝜃))
Assertion
Ref Expression
syl3anbrc (𝜑𝜏)

Proof of Theorem syl3anbrc
StepHypRef Expression
1 syl3anbrc.1 . . 3 (𝜑𝜓)
2 syl3anbrc.2 . . 3 (𝜑𝜒)
3 syl3anbrc.3 . . 3 (𝜑𝜃)
41, 2, 33jca 1240 . 2 (𝜑 → (𝜓𝜒𝜃))
5 syl3anbrc.4 . 2 (𝜏 ↔ (𝜓𝜒𝜃))
64, 5sylibr 224 1 (𝜑𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  w3a 1036
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 197  df-an 386  df-3an 1038
This theorem is referenced by:  soisores  6542  limuni3  7014  onfununi  7398  smores2  7411  smoiso  7419  oelimcl  7640  iserd  7728  erinxp  7781  resixp  7903  undifixp  7904  alephval3  8893  fpwwe2lem12  9423  canthwelem  9432  canthwe  9433  r1limwun  9518  wunex2  9520  tskcard  9563  gruina  9600  nqerf  9712  nqerid  9715  eluzmn  11654  eluzuzle  11656  uztrn  11664  nn0pzuz  11705  zsupss  11737  nn0ge2m1nnALT  11742  xov1plusxeqvd  12276  ssfzunsnext  12344  ige2m1fz  12387  0elfz  12393  uzsubfz0  12404  elfzmlbm  12406  difelfzle  12409  difelfznle  12410  fvffz0  12414  elfzolt2b  12438  elfzolt3b  12439  elfzouz2  12441  fzossrbm1  12454  elfzo0  12465  eluzgtdifelfzo  12486  elfzodifsumelfzo  12490  fzonn0p1  12501  fzonn0p1p1  12503  elfzom1p1elfzo  12504  fzo0sn0fzo1  12514  ssfzo12bi  12520  ubmelm1fzo  12521  elfzonelfzo  12527  fzosplitprm1  12534  fzostep1  12540  fvinim0ffz  12543  flword2  12570  uzsup  12618  modfzo0difsn  12698  modsumfzodifsn  12699  fsuppmapnn0fiub  12746  fsuppmapnn0fiubOLD  12747  suppssfz  12750  1elfz0hash  13135  fzsdom2  13171  ccatrn  13327  swrdn0  13384  swrdtrcfv  13395  swrdtrcfv0  13396  swrdeq  13398  swrdtrcfvl  13404  swrdswrd  13414  swrdccatwrd  13422  wrdeqs1cat  13428  swrdccatin1  13436  swrdccat3  13445  swrdccatid  13450  repswswrd  13484  cshwidxmod  13502  cshw1  13521  cshwcsh2id  13527  swrds2  13635  2swrd2eqwrdeq  13646  ccat2s1fvwALT  13648  rexuzre  14042  limsupgre  14162  rlimclim1  14226  rlimclim  14227  climrlim2  14228  isercolllem1  14345  isercoll  14348  climcndslem1  14525  fallfacval4  14718  tanhbnd  14835  sinbnd2  14856  cosbnd2  14857  rpnnen2lem12  14898  nn0o  15042  bitsfzolem  15099  bitsfzo  15100  bitsmod  15101  bitsfi  15102  bitsinv1lem  15106  bitsinv1  15107  smueqlem  15155  dvdsnprmd  15346  hashgcdlem  15436  prm23lt5  15462  zgz  15580  gznegcl  15582  gzcjcl  15583  gzaddcl  15584  gzmulcl  15585  vdwlem9  15636  prmgaplem3  15700  prmgaplem4  15701  cshwshashlem2  15746  setsstruct2  15836  ismred  16202  isfuncd  16465  homdmcoa  16657  isdrs2  16879  fpwipodrs  17104  ipodrsima  17105  psss  17154  psssdm2  17155  sgrp2rid2ex  17354  subgid  17536  issubg2  17549  subsubg  17557  gaorber  17681  orbsta  17686  pmtrfconj  17826  psgnunilem2  17855  psgnunilem3  17856  psgnunilem4  17857  pgpfi1  17950  subgpgp  17952  pgpssslw  17969  subgslw  17971  sylow2alem2  17973  fislw  17980  sylow3lem3  17984  efgs1  18088  efgsp1  18090  efgsres  18091  efgredleme  18096  efgcpbllemb  18108  lt6abl  18236  telgsumfzs  18326  ablfac1eu  18412  isringd  18525  ringsrg  18529  ring1  18542  prdsringd  18552  subrgsubg  18726  islmodd  18809  islssd  18876  islss4  18902  gsummoncoe1  19614  gzrngunit  19752  expmhm  19755  zringunit  19776  prmirredlem  19781  znidomb  19850  isphld  19939  ocvocv  19955  ocvlss  19956  frlmlbs  20076  mp2pm2mplem4  20554  chfacfisf  20599  chfacfisfcpmat  20600  chfacfscmulfsupp  20604  chfacfpmmulfsupp  20608  chfacfpmmulgsum2  20610  2ndcctbss  21198  finlocfin  21263  dissnlocfin  21272  locfindis  21273  locfincf  21274  isfild  21602  infil  21607  neifil  21624  flimfcls  21770  istgp2  21835  oppgtmd  21841  oppgtgp  21842  distgp  21843  indistgp  21844  symgtgp  21845  submtmd  21848  subgtgp  21849  qustgplem  21864  prdstmdd  21867  prdstgpd  21868  tlmtgp  21939  isngp4  22356  subgngp  22379  ngptgp  22380  tngngp2  22396  nrgtrg  22434  nrgtdrg  22437  elii2  22675  icopnfcnv  22681  xrhmeo  22685  lebnumii  22705  phtpcer  22734  phtpcerOLD  22735  reparpht  22738  phtpcco2  22739  pcohtpy  22760  pcoass  22764  pcorevlem  22766  pi1cpbl  22784  pi1grplem  22789  isclmi  22817  isncvsngpd  22890  cphsubrglem  22917  cphclm  22929  tchclm  22971  tchcph  22976  clsocv  22989  pjthlem2  23149  ovolf  23190  iundisj2  23257  vitalilem2  23318  vitali  23322  itg2monolem3  23459  dvfsumlem1  23727  dvfsumlem3  23729  mon1puc1p  23848  uc1pmon1p  23849  ply1remlem  23860  drnguc1p  23868  plyaddlem1  23907  coeidlem  23931  aannenlem2  24022  radcnvcl  24109  pilem2  24144  coseq00topi  24192  coseq0negpitopi  24193  tangtx  24195  tanabsge  24196  cosq14gt0  24200  cosq14ge0  24201  cosordlem  24215  sinord  24218  resinf1o  24220  tanord1  24221  tanord  24222  efif1olem3  24228  efsubm  24235  relogrn  24246  logimclad  24257  logrnaddcl  24259  logneg  24272  logcj  24290  argregt0  24294  argrege0  24295  argimgt0  24296  argimlt0  24297  logimul  24298  logneg2  24299  logdmnrp  24321  logcnlem4  24325  dvloglem  24328  logf1o2  24330  efopnlem2  24337  cxpsqrtlem  24382  relogbval  24444  nnlogbexp  24453  relogbcxp  24457  relogbcxpb  24459  asinneg  24547  asinsin  24553  acoscos  24554  acosbnd  24561  atancj  24571  atanlogaddlem  24574  atanlogsublem  24576  atanlogsub  24577  atantan  24584  atanbndlem  24586  atans2  24592  leibpi  24603  scvxcvx  24646  jensenlem2  24648  emcllem7  24662  basellem1  24741  ppisval  24764  chtdif  24818  ppidif  24823  ppiub  24863  chtublem  24870  chtub  24871  lgsdilem2  24992  gausslemma2dlem1a  25024  gausslemma2dlem2  25026  gausslemma2dlem5  25030  gausslemma2dlem6  25031  lgsquadlem1  25039  lgsquadlem2  25040  lgsquadlem3  25041  2lgslem1  25053  2sqlem3  25079  chebbnd1lem1  25092  chebbnd1lem2  25093  chebbnd1lem3  25094  dchrisumlem2  25113  dchrvmasumlem2  25121  dchrvmasumiflem1  25124  dchrisum0flblem2  25132  mulog2sumlem2  25158  logdivbnd  25179  pntpbnd2  25210  pntibndlem1  25212  pntibnd  25216  pntlemc  25218  pntlemg  25221  pntlemq  25224  pntlemf  25228  padicabvf  25254  padicabvcxp  25255  ostth2  25260  ttgcontlem1  25699  axpaschlem  25754  pthdadjvtx  26529  pthdlem1  26565  pthd  26568  crctcshwlkn0lem3  26607  crctcshwlkn0lem4  26608  crctcshwlkn0lem5  26609  crctcshwlkn0lem7  26611  wlkiswwlks1  26656  wwlksm1edg  26670  wwlksnred  26690  wwlksnredwwlkn  26693  wwlksnextproplem3  26709  clwlkclwwlklem2fv1  26797  clwlkclwwlklem2fv2  26798  clwlkclwwlklem2a  26800  clwlkclwwlklem2  26802  clwwlksel  26814  clwwlksf  26815  wwlksext2clwwlk  26824  wwlksubclwwlks  26825  clwwisshclwwslemlem  26826  clwwisshclwwslem  26827  erclwwlksref  26834  umgr2cwwkdifex  26842  clwlksfclwwlk  26862  1pthd  26903  eucrctshift  27003  extwwlkfablem2  27102  numclwlk2lem2f  27125  frgrreggt1  27139  grpoinvf  27274  strlem3a  28999  hstrlem3a  29007  iundisj2f  29289  fcoinver  29302  ssnnssfz  29432  bcm1n  29437  iundisj2fi  29439  fsumrp0cl  29522  submomnd  29537  lmodslmd  29584  suborng  29642  locfinreflem  29731  locfinref  29732  xrge0iifcnv  29803  xrge0iifiso  29805  xrge0iifhom  29807  esumc  29936  esumle  29943  esumlef  29947  esumpinfsum  29962  esumpcvgval  29963  fiunelros  30060  voliune  30115  volfiniune  30116  sibfinima  30224  eulerpartlemt  30256  fiblem  30283  fibp1  30286  dstrvprob  30356  ballotlemsel1i  30397  ballotlemfrceq  30413  plymulx0  30446  signstfvc  30473  signstfveq0  30476  bnj944  30769  bnj998  30787  bnj1136  30826  bnj1408  30865  erdszelem4  30937  erdszelem8  30941  txsconnlem  30983  cvxsconn  30986  cvmliftpht  31061  snmlff  31072  elmrsubrn  31178  msrf  31200  mthmpps  31240  sinccvglem  31327  noextend  31577  nosino  31628  trer  32005  poimirlem6  33086  poimirlem7  33087  poimirlem9  33089  poimirlem17  33097  poimirlem20  33100  poimirlem28  33108  poimirlem29  33109  poimirlem30  33110  poimirlem31  33111  poimirlem32  33112  areacirc  33176  nnubfi  33217  prter1  33683  lkrlss  33901  diaf11N  35857  dibf11N  35969  lclkr  36341  lclkrs  36347  lcfrlem9  36358  lcfr  36393  mapd1o  36456  hdmapf1oN  36676  hgmapf1oN  36714  nacsfix  36794  eldioph2lem1  36842  irrapxlem1  36905  rmxypairf1o  36995  jm2.27a  37091  hbtlem2  37214  hbt  37220  cntzsdrg  37292  mon1pid  37303  mon1psubm  37304  binomcxplemnotnn0  38076  elfzfzo  38987  monoords  39010  elfzod  39123  eluzd  39134  fmul01lt1lem2  39253  sumnnodd  39298  ioodvbdlimc1lem2  39484  ioodvbdlimc2lem  39486  iblsplit  39519  iblspltprt  39526  itgspltprt  39532  stoweidlem11  39565  stoweidlem17  39571  fourierdlem12  39673  fourierdlem20  39681  fourierdlem25  39686  fourierdlem37  39698  fourierdlem41  39702  fourierdlem48  39708  fourierdlem49  39709  fourierdlem50  39710  fourierdlem54  39714  fourierdlem64  39724  fourierdlem73  39733  fourierdlem79  39739  fourierdlem102  39762  fourierdlem111  39771  fourierdlem114  39774  etransclem23  39811  etransclem48  39836  2elfz2melfz  40655  elfzlble  40657  fzoopth  40664  iccpartiltu  40686  iccpartigtl  40687  iccpartlt  40688  iccpartgt  40691  lswn0  40708  pfxtrcfv0  40731  pfxeq  40733  pfxtrcfvl  40734  pfx2  40741  pfxccat3  40755  pfxccat3a  40758  fmtnoge3  40771  fmtnodvds  40785  odz2prm2pw  40804  fmtnole4prm  40819  lighneallem4b  40855  nnsum4primesevenALTV  41008  bgoldbtbndlem3  41014  ringrng  41197  isringrng  41199  lidlrng  41245  ssnn0ssfz  41445  lmod1  41599  elfzolborelfzop1  41627  nnolog2flm1  41706
  Copyright terms: Public domain W3C validator