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

Theorem syl3anbrc 1429
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 1123 . 2 (𝜑 → (𝜓𝜒𝜃))
5 syl3anbrc.4 . 2 (𝜏 ↔ (𝜓𝜒𝜃))
64, 5sylibr 224 1 (𝜑𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  w3a 1072
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 1074
This theorem is referenced by:  soisores  6740  limuni3  7217  onfununi  7607  smores2  7620  smoiso  7628  oelimcl  7849  iserd  7937  erinxp  7988  resixp  8109  undifixp  8110  alephval3  9123  fpwwe2lem12  9655  canthwelem  9664  canthwe  9665  r1limwun  9750  wunex2  9752  tskcard  9795  gruina  9832  nqerf  9944  nqerid  9947  eluzmn  11886  eluzuzle  11888  uztrn  11896  subeluzsub  11910  nn0pzuz  11938  zsupss  11970  nn0ge2m1nnALT  11975  xov1plusxeqvd  12511  ssfzunsnext  12579  ige2m1fz  12623  0elfz  12630  uzsubfz0  12641  elfzmlbm  12643  difelfzle  12646  difelfznle  12647  fvffz0  12651  elfzolt2b  12675  elfzolt3b  12676  elfzouz2  12678  fzossrbm1  12691  elfzo0  12703  eluzgtdifelfzo  12724  elfzodifsumelfzo  12728  fzonn0p1  12739  fzonn0p1p1  12741  elfzom1p1elfzo  12742  fzo0sn0fzo1  12751  ssfzo12bi  12757  ubmelm1fzo  12758  elfzonelfzo  12764  fzosplitprm1  12772  fzostep1  12778  fvinim0ffz  12781  flword2  12808  uzsup  12856  modfzo0difsn  12936  modsumfzodifsn  12937  fsuppmapnn0fiub  12984  fsuppmapnn0fiubOLD  12985  suppssfz  12988  1elfz0hash  13371  fzsdom2  13407  ccatrn  13561  swrdn0  13630  swrdtrcfv  13641  swrdtrcfv0  13642  swrdeq  13644  swrdtrcfvl  13650  swrdswrd  13660  swrdccatwrd  13668  wrdeqs1cat  13674  swrdccatin1  13683  swrdccat3  13692  swrdccatid  13697  repswswrd  13731  cshwidxmod  13749  cshw1  13768  cshwcsh2id  13774  swrds2  13885  2swrd2eqwrdeq  13897  ccat2s1fvwALT  13899  rexuzre  14291  limsupgre  14411  rlimclim1  14475  rlimclim  14476  climrlim2  14477  isercolllem1  14594  isercoll  14597  climcndslem1  14780  fallfacval4  14973  tanhbnd  15090  sinbnd2  15111  cosbnd2  15112  rpnnen2lem12  15153  nn0o  15301  bitsfzolem  15358  bitsfzo  15359  bitsmod  15360  bitsfi  15361  bitsinv1lem  15365  bitsinv1  15366  smueqlem  15414  dvdsnprmd  15605  hashgcdlem  15695  prm23lt5  15721  zgz  15839  gznegcl  15841  gzcjcl  15842  gzaddcl  15843  gzmulcl  15844  vdwlem9  15895  prmgaplem3  15959  prmgaplem4  15960  cshwshashlem2  16005  setsstruct2  16098  ismred  16464  isfuncd  16726  homdmcoa  16918  isdrs2  17140  fpwipodrs  17365  ipodrsima  17366  psss  17415  psssdm2  17416  sgrp2rid2ex  17615  subgid  17797  issubg2  17810  subsubg  17818  gaorber  17941  orbsta  17946  pmtrfconj  18086  psgnunilem2  18115  psgnunilem3  18116  psgnunilem4  18117  pgpfi1  18210  subgpgp  18212  pgpssslw  18229  subgslw  18231  sylow2alem2  18233  fislw  18240  sylow3lem3  18244  efgs1  18348  efgsp1  18350  efgsres  18351  efgredleme  18356  efgcpbllemb  18368  lt6abl  18496  telgsumfzs  18586  ablfac1eu  18672  isringd  18785  ringsrg  18789  ring1  18802  prdsringd  18812  subrgsubg  18988  islmodd  19071  islssd  19138  islss4  19164  gsummoncoe1  19876  gzrngunit  20014  expmhm  20017  zringunit  20038  prmirredlem  20043  znidomb  20112  isphld  20201  ocvocv  20217  ocvlss  20218  frlmlbs  20338  mp2pm2mplem4  20816  chfacfisf  20861  chfacfisfcpmat  20862  chfacfscmulfsupp  20866  chfacfpmmulfsupp  20870  chfacfpmmulgsum2  20872  2ndcctbss  21460  finlocfin  21525  dissnlocfin  21534  locfindis  21535  locfincf  21536  isfild  21863  infil  21868  neifil  21885  flimfcls  22031  istgp2  22096  oppgtmd  22102  oppgtgp  22103  distgp  22104  indistgp  22105  symgtgp  22106  submtmd  22109  subgtgp  22110  qustgplem  22125  prdstmdd  22128  prdstgpd  22129  tlmtgp  22200  isngp4  22617  subgngp  22640  ngptgp  22641  tngngp2  22657  nrgtrg  22695  nrgtdrg  22698  elii2  22936  icopnfcnv  22942  xrhmeo  22946  lebnumii  22966  phtpcer  22995  reparpht  22998  phtpcco2  22999  pcohtpy  23020  pcoass  23024  pcorevlem  23026  pi1cpbl  23044  pi1grplem  23049  isclmi  23077  isncvsngpd  23150  cphsubrglem  23177  cphclm  23189  tchclm  23231  tchcph  23236  clsocv  23249  pjthlem2  23409  ovolf  23450  iundisj2  23517  vitalilem2  23577  vitali  23581  itg2monolem3  23718  dvfsumlem1  23988  dvfsumlem3  23990  mon1puc1p  24109  uc1pmon1p  24110  ply1remlem  24121  drnguc1p  24129  plyaddlem1  24168  coeidlem  24192  aannenlem2  24283  radcnvcl  24370  pilem2  24405  coseq00topi  24453  coseq0negpitopi  24454  tangtx  24456  tanabsge  24457  cosq14gt0  24461  cosq14ge0  24462  cosordlem  24476  sinord  24479  resinf1o  24481  tanord1  24482  tanord  24483  efif1olem3  24489  efsubm  24496  relogrn  24507  logimclad  24518  logrnaddcl  24520  logneg  24533  logcj  24551  argregt0  24555  argrege0  24556  argimgt0  24557  argimlt0  24558  logimul  24559  logneg2  24560  logdmnrp  24586  logcnlem4  24590  dvloglem  24593  logf1o2  24595  efopnlem2  24602  cxpsqrtlem  24647  relogbval  24709  nnlogbexp  24718  relogbcxp  24722  relogbcxpb  24724  asinneg  24812  asinsin  24818  acoscos  24819  acosbnd  24826  atancj  24836  atanlogaddlem  24839  atanlogsublem  24841  atanlogsub  24842  atantan  24849  atanbndlem  24851  atans2  24857  leibpi  24868  scvxcvx  24911  jensenlem2  24913  emcllem7  24927  basellem1  25006  ppisval  25029  chtdif  25083  ppidif  25088  ppiub  25128  chtublem  25135  chtub  25136  lgsdilem2  25257  gausslemma2dlem1a  25289  gausslemma2dlem2  25291  gausslemma2dlem5  25295  gausslemma2dlem6  25296  lgsquadlem1  25304  lgsquadlem2  25305  lgsquadlem3  25306  2lgslem1  25318  2sqlem3  25344  chebbnd1lem1  25357  chebbnd1lem2  25358  chebbnd1lem3  25359  dchrisumlem2  25378  dchrvmasumlem2  25386  dchrvmasumiflem1  25389  dchrisum0flblem2  25397  mulog2sumlem2  25423  logdivbnd  25444  pntpbnd2  25475  pntibndlem1  25477  pntibnd  25481  pntlemc  25483  pntlemg  25486  pntlemq  25489  pntlemf  25493  padicabvf  25519  padicabvcxp  25520  ostth2  25525  ttgcontlem1  25964  axpaschlem  26019  nbgr2vtx1edg  26445  nbuhgr2vtx1edgb  26447  cusgrexi  26549  structtocusgr  26552  pthdadjvtx  26836  pthdlem1  26872  pthd  26875  crctcshwlkn0lem3  26915  crctcshwlkn0lem4  26916  crctcshwlkn0lem5  26917  crctcshwlkn0lem7  26919  wlkiswwlks1  26976  wwlksm1edg  26990  wwlksnred  27010  wwlksnredwwlkn  27013  wwlksnextproplem3  27029  clwlkclwwlklem2fv1  27118  clwlkclwwlklem2fv2  27119  clwlkclwwlklem2a  27121  clwlkclwwlklem2  27123  clwwisshclwwslemlem  27136  clwwisshclwwslem  27137  erclwwlkref  27143  clwwlkel  27175  clwwlkf  27176  wwlksext2clwwlk  27187  wwlksext2clwwlkOLD  27188  wwlksubclwwlk  27189  umgr2cwwkdifex  27196  clwlksfclwwlkOLD  27216  1pthd  27295  eucrctshift  27395  dlwwlknonclwlknonf1olem1  27524  numclwlk2lem2f  27538  numclwlk2lem2fOLD  27545  frgrreggt1  27561  grpoinvf  27695  strlem3a  29420  hstrlem3a  29428  iundisj2f  29710  fcoinver  29725  ssnnssfz  29858  bcm1n  29863  iundisj2fi  29865  fsumrp0cl  30004  submomnd  30019  lmodslmd  30066  suborng  30124  locfinreflem  30216  locfinref  30217  xrge0iifcnv  30288  xrge0iifiso  30290  xrge0iifhom  30292  esumc  30422  esumle  30429  esumlef  30433  esumpinfsum  30448  esumpcvgval  30449  fiunelros  30546  voliune  30601  volfiniune  30602  sibfinima  30710  eulerpartlemt  30742  fiblem  30769  fibp1  30772  dstrvprob  30842  ballotlemsel1i  30883  ballotlemfrceq  30899  plymulx0  30933  signstfvc  30960  signstfveq0  30963  bnj944  31315  bnj998  31333  bnj1136  31372  bnj1408  31411  erdszelem4  31483  erdszelem8  31487  txsconnlem  31529  cvxsconn  31532  cvmliftpht  31607  snmlff  31618  elmrsubrn  31724  msrf  31746  mthmpps  31786  sinccvglem  31873  noextend  32125  noextendseq  32126  nosupno  32155  trer  32616  poimirlem6  33728  poimirlem7  33729  poimirlem9  33731  poimirlem17  33739  poimirlem20  33742  poimirlem28  33750  poimirlem29  33751  poimirlem30  33752  poimirlem31  33753  poimirlem32  33754  areacirc  33818  nnubfi  33859  prter1  34668  lkrlss  34885  diaf11N  36840  dibf11N  36952  lclkr  37324  lclkrs  37330  lcfrlem9  37341  lcfr  37376  mapd1o  37439  hdmapf1oN  37659  hgmapf1oN  37697  nacsfix  37777  eldioph2lem1  37825  irrapxlem1  37888  rmxypairf1o  37978  jm2.27a  38074  hbtlem2  38196  hbt  38202  cntzsdrg  38274  mon1pid  38285  mon1psubm  38286  binomcxplemnotnn0  39057  elfzfzo  39987  monoords  40010  elfzod  40122  eluzd  40133  fmul01lt1lem2  40320  sumnnodd  40365  ioodvbdlimc1lem2  40650  ioodvbdlimc2lem  40652  iblsplit  40685  iblspltprt  40692  itgspltprt  40698  stoweidlem11  40731  stoweidlem17  40737  fourierdlem12  40839  fourierdlem20  40847  fourierdlem25  40852  fourierdlem37  40864  fourierdlem41  40868  fourierdlem48  40874  fourierdlem49  40875  fourierdlem50  40876  fourierdlem54  40880  fourierdlem64  40890  fourierdlem73  40899  fourierdlem79  40905  fourierdlem102  40928  fourierdlem111  40937  fourierdlem114  40940  etransclem23  40977  etransclem48  41002  2elfz2melfz  41838  elfzlble  41840  fzoopth  41847  iccpartiltu  41868  iccpartigtl  41869  iccpartlt  41870  iccpartgt  41873  lswn0  41890  pfxtrcfv0  41912  pfxeq  41914  pfxtrcfvl  41915  pfx2  41922  pfxccat3  41936  pfxccat3a  41939  fmtnoge3  41952  fmtnodvds  41966  odz2prm2pw  41985  fmtnole4prm  42000  lighneallem4b  42036  mogoldbb  42183  nnsum4primesevenALTV  42199  bgoldbtbndlem3  42205  ringrng  42389  isringrng  42391  lidlrng  42437  ssnn0ssfz  42637  lmod1  42791  elfzolborelfzop1  42819  nnolog2flm1  42894
  Copyright terms: Public domain W3C validator