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

Theorem syl3anbrc 1265
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 1261 . 2 (𝜑 → (𝜓𝜒𝜃))
5 syl3anbrc.4 . 2 (𝜏 ↔ (𝜓𝜒𝜃))
64, 5sylibr 224 1 (𝜑𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  w3a 1054
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 385  df-3an 1056
This theorem is referenced by:  soisores  6617  limuni3  7094  onfununi  7483  smores2  7496  smoiso  7504  oelimcl  7725  iserd  7813  erinxp  7864  resixp  7985  undifixp  7986  alephval3  8971  fpwwe2lem12  9501  canthwelem  9510  canthwe  9511  r1limwun  9596  wunex2  9598  tskcard  9641  gruina  9678  nqerf  9790  nqerid  9793  eluzmn  11732  eluzuzle  11734  uztrn  11742  nn0pzuz  11783  zsupss  11815  nn0ge2m1nnALT  11820  xov1plusxeqvd  12356  ssfzunsnext  12424  ige2m1fz  12468  0elfz  12475  uzsubfz0  12486  elfzmlbm  12488  difelfzle  12491  difelfznle  12492  fvffz0  12496  elfzolt2b  12520  elfzolt3b  12521  elfzouz2  12523  fzossrbm1  12536  elfzo0  12548  eluzgtdifelfzo  12569  elfzodifsumelfzo  12573  fzonn0p1  12584  fzonn0p1p1  12586  elfzom1p1elfzo  12587  fzo0sn0fzo1  12597  ssfzo12bi  12603  ubmelm1fzo  12604  elfzonelfzo  12610  fzosplitprm1  12618  fzostep1  12624  fvinim0ffz  12627  flword2  12654  uzsup  12702  modfzo0difsn  12782  modsumfzodifsn  12783  fsuppmapnn0fiub  12830  fsuppmapnn0fiubOLD  12831  suppssfz  12834  1elfz0hash  13217  fzsdom2  13253  ccatrn  13407  swrdn0  13476  swrdtrcfv  13487  swrdtrcfv0  13488  swrdeq  13490  swrdtrcfvl  13496  swrdswrd  13506  swrdccatwrd  13514  wrdeqs1cat  13520  swrdccatin1  13529  swrdccat3  13538  swrdccatid  13543  repswswrd  13577  cshwidxmod  13595  cshw1  13614  cshwcsh2id  13620  swrds2  13731  2swrd2eqwrdeq  13742  ccat2s1fvwALT  13744  rexuzre  14136  limsupgre  14256  rlimclim1  14320  rlimclim  14321  climrlim2  14322  isercolllem1  14439  isercoll  14442  climcndslem1  14625  fallfacval4  14818  tanhbnd  14935  sinbnd2  14956  cosbnd2  14957  rpnnen2lem12  14998  nn0o  15146  bitsfzolem  15203  bitsfzo  15204  bitsmod  15205  bitsfi  15206  bitsinv1lem  15210  bitsinv1  15211  smueqlem  15259  dvdsnprmd  15450  hashgcdlem  15540  prm23lt5  15566  zgz  15684  gznegcl  15686  gzcjcl  15687  gzaddcl  15688  gzmulcl  15689  vdwlem9  15740  prmgaplem3  15804  prmgaplem4  15805  cshwshashlem2  15850  setsstruct2  15943  ismred  16309  isfuncd  16572  homdmcoa  16764  isdrs2  16986  fpwipodrs  17211  ipodrsima  17212  psss  17261  psssdm2  17262  sgrp2rid2ex  17461  subgid  17643  issubg2  17656  subsubg  17664  gaorber  17787  orbsta  17792  pmtrfconj  17932  psgnunilem2  17961  psgnunilem3  17962  psgnunilem4  17963  pgpfi1  18056  subgpgp  18058  pgpssslw  18075  subgslw  18077  sylow2alem2  18079  fislw  18086  sylow3lem3  18090  efgs1  18194  efgsp1  18196  efgsres  18197  efgredleme  18202  efgcpbllemb  18214  lt6abl  18342  telgsumfzs  18432  ablfac1eu  18518  isringd  18631  ringsrg  18635  ring1  18648  prdsringd  18658  subrgsubg  18834  islmodd  18917  islssd  18984  islss4  19010  gsummoncoe1  19722  gzrngunit  19860  expmhm  19863  zringunit  19884  prmirredlem  19889  znidomb  19958  isphld  20047  ocvocv  20063  ocvlss  20064  frlmlbs  20184  mp2pm2mplem4  20662  chfacfisf  20707  chfacfisfcpmat  20708  chfacfscmulfsupp  20712  chfacfpmmulfsupp  20716  chfacfpmmulgsum2  20718  2ndcctbss  21306  finlocfin  21371  dissnlocfin  21380  locfindis  21381  locfincf  21382  isfild  21709  infil  21714  neifil  21731  flimfcls  21877  istgp2  21942  oppgtmd  21948  oppgtgp  21949  distgp  21950  indistgp  21951  symgtgp  21952  submtmd  21955  subgtgp  21956  qustgplem  21971  prdstmdd  21974  prdstgpd  21975  tlmtgp  22046  isngp4  22463  subgngp  22486  ngptgp  22487  tngngp2  22503  nrgtrg  22541  nrgtdrg  22544  elii2  22782  icopnfcnv  22788  xrhmeo  22792  lebnumii  22812  phtpcer  22841  reparpht  22844  phtpcco2  22845  pcohtpy  22866  pcoass  22870  pcorevlem  22872  pi1cpbl  22890  pi1grplem  22895  isclmi  22923  isncvsngpd  22996  cphsubrglem  23023  cphclm  23035  tchclm  23077  tchcph  23082  clsocv  23095  pjthlem2  23255  ovolf  23296  iundisj2  23363  vitalilem2  23423  vitali  23427  itg2monolem3  23564  dvfsumlem1  23834  dvfsumlem3  23836  mon1puc1p  23955  uc1pmon1p  23956  ply1remlem  23967  drnguc1p  23975  plyaddlem1  24014  coeidlem  24038  aannenlem2  24129  radcnvcl  24216  pilem2  24251  coseq00topi  24299  coseq0negpitopi  24300  tangtx  24302  tanabsge  24303  cosq14gt0  24307  cosq14ge0  24308  cosordlem  24322  sinord  24325  resinf1o  24327  tanord1  24328  tanord  24329  efif1olem3  24335  efsubm  24342  relogrn  24353  logimclad  24364  logrnaddcl  24366  logneg  24379  logcj  24397  argregt0  24401  argrege0  24402  argimgt0  24403  argimlt0  24404  logimul  24405  logneg2  24406  logdmnrp  24432  logcnlem4  24436  dvloglem  24439  logf1o2  24441  efopnlem2  24448  cxpsqrtlem  24493  relogbval  24555  nnlogbexp  24564  relogbcxp  24568  relogbcxpb  24570  asinneg  24658  asinsin  24664  acoscos  24665  acosbnd  24672  atancj  24682  atanlogaddlem  24685  atanlogsublem  24687  atanlogsub  24688  atantan  24695  atanbndlem  24697  atans2  24703  leibpi  24714  scvxcvx  24757  jensenlem2  24759  emcllem7  24773  basellem1  24852  ppisval  24875  chtdif  24929  ppidif  24934  ppiub  24974  chtublem  24981  chtub  24982  lgsdilem2  25103  gausslemma2dlem1a  25135  gausslemma2dlem2  25137  gausslemma2dlem5  25141  gausslemma2dlem6  25142  lgsquadlem1  25150  lgsquadlem2  25151  lgsquadlem3  25152  2lgslem1  25164  2sqlem3  25190  chebbnd1lem1  25203  chebbnd1lem2  25204  chebbnd1lem3  25205  dchrisumlem2  25224  dchrvmasumlem2  25232  dchrvmasumiflem1  25235  dchrisum0flblem2  25243  mulog2sumlem2  25269  logdivbnd  25290  pntpbnd2  25321  pntibndlem1  25323  pntibnd  25327  pntlemc  25329  pntlemg  25332  pntlemq  25335  pntlemf  25339  padicabvf  25365  padicabvcxp  25366  ostth2  25371  ttgcontlem1  25810  axpaschlem  25865  nbgr2vtx1edg  26291  nbuhgr2vtx1edgb  26293  cusgrexi  26395  structtocusgr  26398  pthdadjvtx  26682  pthdlem1  26718  pthd  26721  crctcshwlkn0lem3  26760  crctcshwlkn0lem4  26761  crctcshwlkn0lem5  26762  crctcshwlkn0lem7  26764  wlkiswwlks1  26821  wwlksm1edg  26835  wwlksnred  26855  wwlksnredwwlkn  26858  wwlksnextproplem3  26874  clwlkclwwlklem2fv1  26961  clwlkclwwlklem2fv2  26962  clwlkclwwlklem2a  26964  clwlkclwwlklem2  26966  clwwisshclwwslemlem  26970  clwwisshclwwslem  26971  erclwwlkref  26977  clwwlkel  27009  clwwlkf  27010  wwlksext2clwwlk  27021  wwlksext2clwwlkOLD  27022  wwlksubclwwlk  27023  umgr2cwwkdifex  27029  clwlksfclwwlk  27049  1pthd  27121  eucrctshift  27221  2clwwlk2clwwlklem2lem2  27329  numclwlk2lem2f  27357  numclwlk2lem2fOLD  27364  frgrreggt1  27380  grpoinvf  27514  strlem3a  29239  hstrlem3a  29247  iundisj2f  29529  fcoinver  29544  ssnnssfz  29677  bcm1n  29682  iundisj2fi  29684  fsumrp0cl  29823  submomnd  29838  lmodslmd  29885  suborng  29943  locfinreflem  30035  locfinref  30036  xrge0iifcnv  30107  xrge0iifiso  30109  xrge0iifhom  30111  esumc  30241  esumle  30248  esumlef  30252  esumpinfsum  30267  esumpcvgval  30268  fiunelros  30365  voliune  30420  volfiniune  30421  sibfinima  30529  eulerpartlemt  30561  fiblem  30588  fibp1  30591  dstrvprob  30661  ballotlemsel1i  30702  ballotlemfrceq  30718  plymulx0  30752  signstfvc  30779  signstfveq0  30782  bnj944  31134  bnj998  31152  bnj1136  31191  bnj1408  31230  erdszelem4  31302  erdszelem8  31306  txsconnlem  31348  cvxsconn  31351  cvmliftpht  31426  snmlff  31437  elmrsubrn  31543  msrf  31565  mthmpps  31605  sinccvglem  31692  noextend  31944  noextendseq  31945  nosupno  31974  trer  32435  poimirlem6  33545  poimirlem7  33546  poimirlem9  33548  poimirlem17  33556  poimirlem20  33559  poimirlem28  33567  poimirlem29  33568  poimirlem30  33569  poimirlem31  33570  poimirlem32  33571  areacirc  33635  nnubfi  33676  prter1  34483  lkrlss  34700  diaf11N  36655  dibf11N  36767  lclkr  37139  lclkrs  37145  lcfrlem9  37156  lcfr  37191  mapd1o  37254  hdmapf1oN  37474  hgmapf1oN  37512  nacsfix  37592  eldioph2lem1  37640  irrapxlem1  37703  rmxypairf1o  37793  jm2.27a  37889  hbtlem2  38011  hbt  38017  cntzsdrg  38089  mon1pid  38100  mon1psubm  38101  binomcxplemnotnn0  38872  elfzfzo  39802  monoords  39825  elfzod  39937  eluzd  39948  fmul01lt1lem2  40135  sumnnodd  40180  ioodvbdlimc1lem2  40465  ioodvbdlimc2lem  40467  iblsplit  40500  iblspltprt  40507  itgspltprt  40513  stoweidlem11  40546  stoweidlem17  40552  fourierdlem12  40654  fourierdlem20  40662  fourierdlem25  40667  fourierdlem37  40679  fourierdlem41  40683  fourierdlem48  40689  fourierdlem49  40690  fourierdlem50  40691  fourierdlem54  40695  fourierdlem64  40705  fourierdlem73  40714  fourierdlem79  40720  fourierdlem102  40743  fourierdlem111  40752  fourierdlem114  40755  etransclem23  40792  etransclem48  40817  2elfz2melfz  41653  elfzlble  41655  fzoopth  41662  iccpartiltu  41683  iccpartigtl  41684  iccpartlt  41685  iccpartgt  41688  lswn0  41705  pfxtrcfv0  41727  pfxeq  41729  pfxtrcfvl  41730  pfx2  41737  pfxccat3  41751  pfxccat3a  41754  fmtnoge3  41767  fmtnodvds  41781  odz2prm2pw  41800  fmtnole4prm  41815  lighneallem4b  41851  mogoldbb  41998  nnsum4primesevenALTV  42014  bgoldbtbndlem3  42020  ringrng  42204  isringrng  42206  lidlrng  42252  ssnn0ssfz  42452  lmod1  42606  elfzolborelfzop1  42634  nnolog2flm1  42709
  Copyright terms: Public domain W3C validator