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

Theorem syl3anbrc 1344
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 1129 . 2 (𝜑 → (𝜓𝜒𝜃))
5 syl3anbrc.4 . 2 (𝜏 ↔ (𝜓𝜒𝜃))
64, 5sylibr 233 1 (𝜑𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  w3a 1088
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 206  df-an 398  df-3an 1090
This theorem is referenced by:  soisores  7269  limuni3  7781  onfununi  8280  smores2  8293  smoiso  8301  oelimcl  8540  iserd  8633  resixp  8830  undifixp  8831  alephval3  10005  canthwelem  10545  canthwe  10546  r1limwun  10631  wunex2  10633  tskcard  10676  gruina  10713  eluzmn  12729  eluzuzle  12731  uztrn  12740  subeluzsub  12755  nn0pzuz  12785  zsupss  12817  nn0ge2m1nnALT  12822  xov1plusxeqvd  13370  ige2m1fz  13486  0elfz  13493  uzsubfz0  13504  elfzmlbm  13506  difelfzle  13509  difelfznle  13510  fvffz0  13514  elfzolt2b  13538  elfzolt3b  13539  elfzouz2  13542  fzossrbm1  13556  elfzo0  13568  eluzgtdifelfzo  13589  elfzodifsumelfzo  13593  fzonn0p1  13604  fzonn0p1p1  13606  fzo0sn0fzo1  13616  ssfzo12bi  13622  ubmelm1fzo  13623  elfzonelfzo  13629  fzosplitprm1  13637  fzostep1  13643  fvinim0ffz  13646  flword2  13673  uzsup  13723  modfzo0difsn  13803  modsumfzodifsn  13804  fsuppmapnn0fiub  13851  suppssfz  13854  1elfz0hash  14244  fzsdom2  14282  ccatrn  14431  ccat2s1fvw  14482  ccat2s1fvwOLD  14483  pfxn0  14532  pfxtrcfv0  14540  pfxtrcfvl  14543  swrdswrd  14551  swrdccatin1  14571  pfxccat3  14580  pfxccat3a  14584  repswswrd  14630  cshwidxmod  14649  cshw1  14668  cshwcsh2id  14675  swrds2  14787  pfx2  14794  2swrd2eqwrdeq  14800  ccat2s1fvwALT  14803  ccat2s1fvwALTOLD  14804  rexuzre  15197  limsupgre  15323  rlimclim1  15387  rlimclim  15388  climrlim2  15389  isercolllem1  15509  isercoll  15512  climcndslem1  15694  fallfacval4  15886  tanhbnd  16003  sinbnd2  16024  cosbnd2  16025  rpnnen2lem12  16067  nn0o  16225  bitsfzolem  16274  bitsfzo  16275  bitsmod  16276  bitsfi  16277  bitsinv1lem  16281  bitsinv1  16282  smueqlem  16330  dvdsnprmd  16526  2mulprm  16529  hashgcdlem  16620  prm23lt5  16646  zgz  16765  gznegcl  16767  gzcjcl  16768  gzaddcl  16769  gzmulcl  16770  vdwlem9  16821  prmgaplem3  16885  prmgaplem4  16886  cshwshashlem2  16929  setsstruct2  17006  ismred  17442  isfuncd  17711  homdmcoa  17913  isdrs2  18155  fpwipodrs  18389  ipodrsima  18390  sgrp2rid2ex  18697  subgid  18889  issubg2  18902  subsubg  18910  gaorber  19047  orbsta  19052  pmtrfconj  19207  psgnunilem2  19236  psgnunilem3  19237  psgnunilem4  19238  pgpfi1  19336  subgpgp  19338  pgpssslw  19355  subgslw  19357  sylow2alem2  19359  fislw  19366  sylow3lem3  19370  efgs1  19476  efgsp1  19478  efgsres  19479  efgredleme  19484  efgcpbllemb  19496  lt6abl  19631  telgsumfzs  19725  ablfac1eu  19811  isringd  19962  ringsrg  19966  ring1  19979  prdsringd  19989  subrgsubg  20181  sdrgid  20215  cntzsdrg  20222  subdrgint  20223  sdrgint  20224  islmodd  20281  islssd  20349  islss4  20376  gzrngunit  20816  expmhm  20819  zringunit  20840  prmirredlem  20846  znidomb  20921  isphld  21011  ocvocv  21028  ocvlss  21029  frlmlbs  21156  gsummoncoe1  21627  mp2pm2mplem4  22110  chfacfisf  22155  chfacfisfcpmat  22156  chfacfscmulfsupp  22160  chfacfpmmulfsupp  22164  chfacfpmmulgsum2  22166  2ndcctbss  22758  finlocfin  22823  dissnlocfin  22832  locfindis  22833  locfincf  22834  isfild  23161  infil  23166  neifil  23183  flimfcls  23329  istgp2  23394  oppgtmd  23400  oppgtgp  23401  distgp  23402  indistgp  23403  efmndtmd  23404  submtmd  23407  subgtgp  23408  symgtgp  23409  qustgplem  23424  prdstmdd  23427  prdstgpd  23428  tlmtgp  23499  isngp4  23920  subgngp  23943  ngptgp  23944  tngngp2  23968  nrgtrg  24006  nrgtdrg  24009  elii2  24251  icopnfcnv  24257  xrhmeo  24261  lebnumii  24281  phtpcer  24310  reparpht  24313  phtpcco2  24314  pcohtpy  24335  pcoass  24339  pcorevlem  24341  isclmi  24392  isncvsngpd  24466  cphsubrglem  24493  cphclm  24505  phclm  24548  tcphcph  24553  clsocv  24566  cphsscph  24567  cmslssbn  24688  pjthlem2  24754  ovolf  24798  iundisj2  24865  vitalilem2  24925  vitali  24929  itg2monolem3  25069  dvfsumlem1  25342  dvfsumlem3  25344  mon1puc1p  25467  uc1pmon1p  25468  ply1remlem  25479  drnguc1p  25487  plyaddlem1  25526  coeidlem  25550  aannenlem2  25641  radcnvcl  25728  pilem2  25763  coseq00topi  25811  coseq0negpitopi  25812  tangtx  25814  tanabsge  25815  cosq14gt0  25819  cosq14ge0  25820  cosq34lt1  25835  cosordlem  25838  cos0pilt1  25840  sinord  25842  resinf1o  25844  tanord1  25845  tanord  25846  efif1olem3  25852  efsubm  25859  relogrn  25869  logimclad  25880  logrnaddcl  25882  logneg  25895  logcj  25913  argregt0  25917  argrege0  25918  argimgt0  25919  argimlt0  25920  logimul  25921  logneg2  25922  logdmnrp  25948  logcnlem4  25952  dvloglem  25955  logf1o2  25957  efopnlem2  25964  cxpsqrtlem  26009  relogbval  26074  nnlogbexp  26083  relogbcxp  26087  relogbcxpb  26089  logbgt0b  26095  asinneg  26188  asinsin  26194  acoscos  26195  acosbnd  26202  atancj  26212  atanlogaddlem  26215  atanlogsublem  26217  atanlogsub  26218  atantan  26225  atanbndlem  26227  atans2  26233  leibpi  26244  scvxcvx  26287  jensenlem2  26289  emcllem7  26303  basellem1  26382  ppisval  26405  chtdif  26459  ppidif  26464  ppiub  26504  chtublem  26511  chtub  26512  lgsdilem2  26633  gausslemma2dlem1a  26665  gausslemma2dlem2  26667  gausslemma2dlem5  26671  gausslemma2dlem6  26672  lgsquadlem1  26680  lgsquadlem2  26681  lgsquadlem3  26682  2lgslem1  26694  2sqlem3  26720  chebbnd1lem1  26769  chebbnd1lem2  26770  chebbnd1lem3  26771  dchrisumlem2  26790  dchrvmasumlem2  26798  dchrvmasumiflem1  26801  dchrisum0flblem2  26809  mulog2sumlem2  26835  logdivbnd  26856  pntpbnd2  26887  pntibndlem1  26889  pntibnd  26893  pntlemc  26895  pntlemg  26898  pntlemq  26901  pntlemf  26905  padicabvf  26931  padicabvcxp  26932  ostth2  26937  noextend  26966  noextendseq  26967  nosupno  27003  noinfno  27018  ttgcontlem1  27662  axpaschlem  27718  nbgr2vtx1edg  28127  nbuhgr2vtx1edgb  28129  cusgrexi  28220  structtocusgr  28223  pthdadjvtx  28507  pthdlem1  28543  pthd  28546  crctcshwlkn0lem3  28586  crctcshwlkn0lem4  28587  crctcshwlkn0lem5  28588  crctcshwlkn0lem7  28590  wlkiswwlks1  28641  wwlksm1edg  28655  wwlksnred  28666  wwlksnredwwlkn  28669  wwlksnextproplem3  28685  clwlkclwwlklem2fv1  28768  clwlkclwwlklem2fv2  28769  clwlkclwwlklem2a  28771  clwlkclwwlklem2  28773  clwwisshclwwslemlem  28786  clwwisshclwwslem  28787  erclwwlkref  28793  clwwlkel  28819  clwwlkf  28820  wwlksext2clwwlk  28830  wwlksubclwwlk  28831  umgr2cwwkdifex  28838  1pthd  28916  eucrctshift  29016  dlwwlknondlwlknonf1olem1  29137  numclwlk2lem2f  29150  frgrreggt1  29166  grpoinvf  29303  strlem3a  31023  hstrlem3a  31031  iundisj2f  31336  fcoinver  31353  fresf1o  31373  ssnnssfz  31515  bcm1n  31523  iundisj2fi  31525  fsumrp0cl  31711  submomnd  31743  cycpmco2lem6  31805  lmodslmd  31864  fldgensdrg  31907  suborng  31934  intlidl  32019  rhmpreimaidl  32020  idlinsubrg  32025  rhmimaidl  32026  ssmxidllem  32058  locfinreflem  32225  locfinref  32226  xrge0iifcnv  32318  xrge0iifiso  32320  xrge0iifhom  32322  esumc  32454  esumle  32461  esumlef  32465  esumpinfsum  32480  esumpcvgval  32481  fiunelros  32577  voliune  32632  volfiniune  32633  sibfinima  32743  eulerpartlemt  32775  fiblem  32802  fibp1  32805  dstrvprob  32875  ballotlemsel1i  32916  ballotlemfrceq  32932  plymulx0  32963  signstfvc  32990  signstfveq0  32993  bnj944  33354  bnj998  33373  bnj1136  33413  bnj1408  33452  erdszelem4  33592  erdszelem8  33596  txsconnlem  33638  cvxsconn  33641  cvmliftpht  33716  snmlff  33727  elmrsubrn  33918  msrf  33940  mthmpps  33980  sinccvglem  34066  trer  34720  poimirlem6  36016  poimirlem7  36017  poimirlem9  36019  poimirlem17  36027  poimirlem20  36030  poimirlem28  36038  poimirlem29  36039  poimirlem30  36040  poimirlem31  36041  poimirlem32  36042  areacirc  36103  nnubfi  36141  prter1  37273  lkrlss  37489  diaf11N  39444  dibf11N  39556  lclkr  39928  lclkrs  39934  lcfrlem9  39945  lcfr  39980  mapd1o  40043  hdmapf1oN  40260  hgmapf1oN  40298  frlmvscadiccat  40618  sn-inelr  40837  nacsfix  40938  eldioph2lem1  40986  irrapxlem1  41048  rmxypairf1o  41138  jm2.27a  41232  hbtlem2  41354  hbt  41360  mon1pid  41435  mon1psubm  41436  onnog  41606  pren2d  41733  binomcxplemnotnn0  42541  elixpconstg  43204  elfzfzo  43409  monoords  43430  elfzod  43534  eluzd  43543  fmul01lt1lem2  43721  sumnnodd  43766  ioodvbdlimc1lem2  44068  ioodvbdlimc2lem  44070  iblsplit  44102  iblspltprt  44109  itgspltprt  44115  stoweidlem11  44147  stoweidlem17  44153  fourierdlem12  44255  fourierdlem20  44263  fourierdlem25  44268  fourierdlem37  44280  fourierdlem41  44284  fourierdlem48  44290  fourierdlem49  44291  fourierdlem50  44292  fourierdlem54  44296  fourierdlem64  44306  fourierdlem73  44315  fourierdlem79  44321  fourierdlem102  44344  fourierdlem111  44353  fourierdlem114  44356  etransclem23  44393  etransclem48  44418  2elfz2melfz  45445  elfzlble  45447  fzoopth  45454  iccpartiltu  45509  iccpartigtl  45510  iccpartlt  45511  iccpartgt  45514  lswn0  45531  fmtnoge3  45617  fmtnodvds  45631  odz2prm2pw  45650  fmtnole4prm  45665  lighneallem4b  45696  mogoldbb  45872  nnsum4primesevenALTV  45888  bgoldbtbndlem3  45894  ringrng  46072  isringrng  46074  lidlrng  46120  ssnn0ssfz  46320  lmod1  46468  elfzolborelfzop1  46495  nnolog2flm1  46571
  Copyright terms: Public domain W3C validator