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

Theorem syl3anbrc 1335
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 1120 . 2 (𝜑 → (𝜓𝜒𝜃))
5 syl3anbrc.4 . 2 (𝜏 ↔ (𝜓𝜒𝜃))
64, 5sylibr 235 1 (𝜑𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  w3a 1079
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 208  df-an 397  df-3an 1081
This theorem is referenced by:  soisores  7069  limuni3  7555  onfununi  7969  smores2  7982  smoiso  7990  oelimcl  8216  iserd  8305  resixp  8486  undifixp  8487  alephval3  9525  canthwelem  10061  canthwe  10062  r1limwun  10147  wunex2  10149  tskcard  10192  gruina  10229  eluzmn  12239  eluzuzle  12241  uztrn  12250  subeluzsub  12264  nn0pzuz  12294  zsupss  12326  nn0ge2m1nnALT  12331  xov1plusxeqvd  12874  ssfzunsnext  12942  ige2m1fz  12987  0elfz  12994  uzsubfz0  13005  elfzmlbm  13007  difelfzle  13010  difelfznle  13011  fvffz0  13015  elfzolt2b  13039  elfzolt3b  13040  elfzouz2  13042  fzossrbm1  13056  elfzo0  13068  eluzgtdifelfzo  13089  elfzodifsumelfzo  13093  fzonn0p1  13104  fzonn0p1p1  13106  fzo0sn0fzo1  13116  ssfzo12bi  13122  ubmelm1fzo  13123  elfzonelfzo  13129  fzosplitprm1  13137  fzostep1  13143  fvinim0ffz  13146  flword2  13173  uzsup  13221  modfzo0difsn  13301  modsumfzodifsn  13302  fsuppmapnn0fiub  13349  suppssfz  13352  1elfz0hash  13741  fzsdom2  13779  ccatrn  13933  ccat2s1fvw  13988  ccat2s1fvwOLD  13989  pfxn0  14038  pfxtrcfv0  14046  pfxtrcfvl  14049  swrdswrd  14057  swrdccatin1  14077  pfxccat3  14086  pfxccat3a  14090  repswswrd  14136  cshwidxmod  14155  cshw1  14174  cshwcsh2id  14180  swrds2  14292  pfx2  14299  2swrd2eqwrdeq  14305  ccat2s1fvwALT  14308  ccat2s1fvwALTOLD  14309  rexuzre  14702  limsupgre  14828  rlimclim1  14892  rlimclim  14893  climrlim2  14894  isercolllem1  15011  isercoll  15014  climcndslem1  15194  fallfacval4  15387  tanhbnd  15504  sinbnd2  15525  cosbnd2  15526  rpnnen2lem12  15568  nn0o  15724  bitsfzolem  15773  bitsfzo  15774  bitsmod  15775  bitsfi  15776  bitsinv1lem  15780  bitsinv1  15781  smueqlem  15829  dvdsnprmd  16024  2mulprm  16027  hashgcdlem  16115  prm23lt5  16141  zgz  16259  gznegcl  16261  gzcjcl  16262  gzaddcl  16263  gzmulcl  16264  vdwlem9  16315  prmgaplem3  16379  prmgaplem4  16380  cshwshashlem2  16420  setsstruct2  16511  ismred  16863  isfuncd  17125  homdmcoa  17317  isdrs2  17539  fpwipodrs  17764  ipodrsima  17765  sgrp2rid2ex  18032  subgid  18221  issubg2  18234  subsubg  18242  gaorber  18378  orbsta  18383  pmtrfconj  18525  psgnunilem2  18554  psgnunilem3  18555  psgnunilem4  18556  pgpfi1  18651  subgpgp  18653  pgpssslw  18670  subgslw  18672  sylow2alem2  18674  fislw  18681  sylow3lem3  18685  efgs1  18792  efgsp1  18794  efgsres  18795  efgredleme  18800  efgcpbllemb  18812  lt6abl  18946  telgsumfzs  19040  ablfac1eu  19126  isringd  19266  ringsrg  19270  ring1  19283  prdsringd  19293  subrgsubg  19472  sdrgid  19506  cntzsdrg  19512  subdrgint  19513  sdrgint  19514  islmodd  19571  islssd  19638  islss4  19665  gsummoncoe1  20402  gzrngunit  20541  expmhm  20544  zringunit  20565  prmirredlem  20570  znidomb  20638  isphld  20728  ocvocv  20745  ocvlss  20746  frlmlbs  20871  mp2pm2mplem4  21347  chfacfisf  21392  chfacfisfcpmat  21393  chfacfscmulfsupp  21397  chfacfpmmulfsupp  21401  chfacfpmmulgsum2  21403  2ndcctbss  21993  finlocfin  22058  dissnlocfin  22067  locfindis  22068  locfincf  22069  isfild  22396  infil  22401  neifil  22418  flimfcls  22564  istgp2  22629  oppgtmd  22635  oppgtgp  22636  distgp  22637  indistgp  22638  symgtgp  22639  submtmd  22642  subgtgp  22643  qustgplem  22658  prdstmdd  22661  prdstgpd  22662  tlmtgp  22733  isngp4  23150  subgngp  23173  ngptgp  23174  tngngp2  23190  nrgtrg  23228  nrgtdrg  23231  elii2  23469  icopnfcnv  23475  xrhmeo  23479  lebnumii  23499  phtpcer  23528  reparpht  23531  phtpcco2  23532  pcohtpy  23553  pcoass  23557  pcorevlem  23559  isclmi  23610  isncvsngpd  23683  cphsubrglem  23710  cphclm  23722  phclm  23764  tcphcph  23769  clsocv  23782  cphsscph  23783  cmslssbn  23904  pjthlem2  23970  ovolf  24012  iundisj2  24079  vitalilem2  24139  vitali  24143  itg2monolem3  24282  dvfsumlem1  24552  dvfsumlem3  24554  mon1puc1p  24673  uc1pmon1p  24674  ply1remlem  24685  drnguc1p  24693  plyaddlem1  24732  coeidlem  24756  aannenlem2  24847  radcnvcl  24934  pilem2  24969  coseq00topi  25017  coseq0negpitopi  25018  tangtx  25020  tanabsge  25021  cosq14gt0  25025  cosq14ge0  25026  cosordlem  25042  sinord  25045  resinf1o  25047  tanord1  25048  tanord  25049  efif1olem3  25055  efsubm  25062  relogrn  25072  logimclad  25083  logrnaddcl  25085  logneg  25098  logcj  25116  argregt0  25120  argrege0  25121  argimgt0  25122  argimlt0  25123  logimul  25124  logneg2  25125  logdmnrp  25151  logcnlem4  25155  dvloglem  25158  logf1o2  25160  efopnlem2  25167  cxpsqrtlem  25212  relogbval  25277  nnlogbexp  25286  relogbcxp  25290  relogbcxpb  25292  logbgt0b  25298  asinneg  25391  asinsin  25397  acoscos  25398  acosbnd  25405  atancj  25415  atanlogaddlem  25418  atanlogsublem  25420  atanlogsub  25421  atantan  25428  atanbndlem  25430  atans2  25436  leibpi  25448  scvxcvx  25491  jensenlem2  25493  emcllem7  25507  basellem1  25586  ppisval  25609  chtdif  25663  ppidif  25668  ppiub  25708  chtublem  25715  chtub  25716  lgsdilem2  25837  gausslemma2dlem1a  25869  gausslemma2dlem2  25871  gausslemma2dlem5  25875  gausslemma2dlem6  25876  lgsquadlem1  25884  lgsquadlem2  25885  lgsquadlem3  25886  2lgslem1  25898  2sqlem3  25924  chebbnd1lem1  25973  chebbnd1lem2  25974  chebbnd1lem3  25975  dchrisumlem2  25994  dchrvmasumlem2  26002  dchrvmasumiflem1  26005  dchrisum0flblem2  26013  mulog2sumlem2  26039  logdivbnd  26060  pntpbnd2  26091  pntibndlem1  26093  pntibnd  26097  pntlemc  26099  pntlemg  26102  pntlemq  26105  pntlemf  26109  padicabvf  26135  padicabvcxp  26136  ostth2  26141  ttgcontlem1  26599  axpaschlem  26654  nbgr2vtx1edg  27060  nbuhgr2vtx1edgb  27062  cusgrexi  27153  structtocusgr  27156  pthdadjvtx  27439  pthdlem1  27475  pthd  27478  crctcshwlkn0lem3  27518  crctcshwlkn0lem4  27519  crctcshwlkn0lem5  27520  crctcshwlkn0lem7  27522  wlkiswwlks1  27573  wwlksm1edg  27587  wwlksnred  27598  wwlksnredwwlkn  27601  wwlksnextproplem3  27618  clwlkclwwlklem2fv1  27701  clwlkclwwlklem2fv2  27702  clwlkclwwlklem2a  27704  clwlkclwwlklem2  27706  clwwisshclwwslemlem  27719  clwwisshclwwslem  27720  erclwwlkref  27726  clwwlkel  27753  clwwlkf  27754  wwlksext2clwwlk  27764  wwlksubclwwlk  27765  umgr2cwwkdifex  27772  1pthd  27850  eucrctshift  27950  dlwwlknondlwlknonf1olem1  28071  numclwlk2lem2f  28084  frgrreggt1  28100  grpoinvf  28237  strlem3a  29957  hstrlem3a  29965  iundisj2f  30269  fcoinver  30286  fresf1o  30305  ssnnssfz  30437  bcm1n  30445  iundisj2fi  30447  fsumrp0cl  30610  submomnd  30639  cycpmco2lem6  30701  lmodslmd  30760  suborng  30816  locfinreflem  31004  locfinref  31005  xrge0iifcnv  31076  xrge0iifiso  31078  xrge0iifhom  31080  esumc  31210  esumle  31217  esumlef  31221  esumpinfsum  31236  esumpcvgval  31237  fiunelros  31333  voliune  31388  volfiniune  31389  sibfinima  31497  eulerpartlemt  31529  fiblem  31556  fibp1  31559  dstrvprob  31629  ballotlemsel1i  31670  ballotlemfrceq  31686  plymulx0  31717  signstfvc  31744  signstfveq0  31747  bnj944  32110  bnj998  32128  bnj1136  32167  bnj1408  32206  erdszelem4  32339  erdszelem8  32343  txsconnlem  32385  cvxsconn  32388  cvmliftpht  32463  snmlff  32474  elmrsubrn  32665  msrf  32687  mthmpps  32727  sinccvglem  32813  noextend  33071  noextendseq  33072  nosupno  33101  trer  33562  poimirlem6  34780  poimirlem7  34781  poimirlem9  34783  poimirlem17  34791  poimirlem20  34794  poimirlem28  34802  poimirlem29  34803  poimirlem30  34804  poimirlem31  34805  poimirlem32  34806  areacirc  34869  nnubfi  34908  prter1  35897  lkrlss  36113  diaf11N  38067  dibf11N  38179  lclkr  38551  lclkrs  38557  lcfrlem9  38568  lcfr  38603  mapd1o  38666  hdmapf1oN  38883  hgmapf1oN  38921  frlmvscadiccat  39025  nacsfix  39189  eldioph2lem1  39237  irrapxlem1  39299  rmxypairf1o  39388  jm2.27a  39482  hbtlem2  39604  hbt  39610  mon1pid  39685  mon1psubm  39686  pren2d  39795  binomcxplemnotnn0  40568  elixpconstg  41235  elfzfzo  41422  monoords  41444  elfzod  41553  eluzd  41562  fmul01lt1lem2  41746  sumnnodd  41791  ioodvbdlimc1lem2  42097  ioodvbdlimc2lem  42099  iblsplit  42131  iblspltprt  42138  itgspltprt  42144  stoweidlem11  42177  stoweidlem17  42183  fourierdlem12  42285  fourierdlem20  42293  fourierdlem25  42298  fourierdlem37  42310  fourierdlem41  42314  fourierdlem48  42320  fourierdlem49  42321  fourierdlem50  42322  fourierdlem54  42326  fourierdlem64  42336  fourierdlem73  42345  fourierdlem79  42351  fourierdlem102  42374  fourierdlem111  42383  fourierdlem114  42386  etransclem23  42423  etransclem48  42448  2elfz2melfz  43399  elfzlble  43401  fzoopth  43408  iccpartiltu  43429  iccpartigtl  43430  iccpartlt  43431  iccpartgt  43434  lswn0  43451  fmtnoge3  43539  fmtnodvds  43553  odz2prm2pw  43572  fmtnole4prm  43587  lighneallem4b  43621  mogoldbb  43797  nnsum4primesevenALTV  43813  bgoldbtbndlem3  43819  efmndtmd  43967  ringrng  44048  isringrng  44050  lidlrng  44096  ssnn0ssfz  44295  lmod1  44445  elfzolborelfzop1  44472  nnolog2flm1  44548
  Copyright terms: Public domain W3C validator