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

Theorem syl3anbrc 1436
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 1151 . 2 (𝜑 → (𝜓𝜒𝜃))
5 syl3anbrc.4 . 2 (𝜏 ↔ (𝜓𝜒𝜃))
64, 5sylibr 225 1 (𝜑𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  soisores  6795  limuni3  7276  onfununi  7668  smores2  7681  smoiso  7689  oelimcl  7911  iserd  7999  resixp  8174  undifixp  8175  alephval3  9210  canthwelem  9751  canthwe  9752  r1limwun  9837  wunex2  9839  tskcard  9882  gruina  9919  eluzmn  11905  eluzuzle  11907  uztrn  11915  subeluzsub  11929  nn0pzuz  11957  zsupss  11990  nn0ge2m1nnALT  11995  xov1plusxeqvd  12535  ssfzunsnext  12603  ige2m1fz  12647  0elfz  12654  uzsubfz0  12665  elfzmlbm  12667  difelfzle  12670  difelfznle  12671  fvffz0  12675  elfzolt2b  12699  elfzolt3b  12700  elfzouz2  12702  fzossrbm1  12715  elfzo0  12727  eluzgtdifelfzo  12748  elfzodifsumelfzo  12752  fzonn0p1  12763  fzonn0p1p1  12765  elfzom1p1elfzo  12766  fzo0sn0fzo1  12775  ssfzo12bi  12781  ubmelm1fzo  12782  elfzonelfzo  12788  fzosplitprm1  12796  fzostep1  12802  fvinim0ffz  12805  flword2  12832  uzsup  12880  modfzo0difsn  12960  modsumfzodifsn  12961  fsuppmapnn0fiub  13008  suppssfz  13011  1elfz0hash  13391  fzsdom2  13426  ccatrn  13580  swrdn0  13648  swrdtrcfv  13659  swrdtrcfv0  13660  swrdeq  13662  swrdtrcfvl  13668  swrdswrd  13678  swrdccatwrd  13686  wrdeqs1cat  13692  swrdccatin1  13701  swrdccat3  13710  swrdccatid  13715  repswswrd  13749  cshwidxmod  13767  cshw1  13786  cshwcsh2id  13792  swrds2  13903  2swrd2eqwrdeq  13915  ccat2s1fvwALT  13917  rexuzre  14309  limsupgre  14429  rlimclim1  14493  rlimclim  14494  climrlim2  14495  isercolllem1  14612  isercoll  14615  climcndslem1  14797  fallfacval4  14988  tanhbnd  15105  sinbnd2  15126  cosbnd2  15127  rpnnen2lem12  15168  nn0o  15313  bitsfzolem  15369  bitsfzo  15370  bitsmod  15371  bitsfi  15372  bitsinv1lem  15376  bitsinv1  15377  smueqlem  15425  dvdsnprmd  15615  hashgcdlem  15704  prm23lt5  15730  zgz  15848  gznegcl  15850  gzcjcl  15851  gzaddcl  15852  gzmulcl  15853  vdwlem9  15904  prmgaplem3  15968  prmgaplem4  15969  cshwshashlem2  16009  setsstruct2  16101  ismred  16461  isfuncd  16723  homdmcoa  16915  isdrs2  17138  fpwipodrs  17363  ipodrsima  17364  sgrp2rid2ex  17613  subgid  17792  issubg2  17805  subsubg  17813  gaorber  17936  orbsta  17941  pmtrfconj  18081  psgnunilem2  18110  psgnunilem3  18111  psgnunilem4  18112  pgpfi1  18205  subgpgp  18207  pgpssslw  18224  subgslw  18226  sylow2alem2  18228  fislw  18235  sylow3lem3  18239  efgs1  18343  efgsp1  18345  efgsres  18346  efgredleme  18351  efgcpbllemb  18363  lt6abl  18491  telgsumfzs  18582  ablfac1eu  18668  isringd  18781  ringsrg  18785  ring1  18798  prdsringd  18808  subrgsubg  18984  islmodd  19067  islssd  19134  islss4  19163  gsummoncoe1  19876  gzrngunit  20014  expmhm  20017  zringunit  20038  prmirredlem  20043  znidomb  20111  isphld  20203  ocvocv  20219  ocvlss  20220  frlmlbs  20340  mp2pm2mplem4  20821  chfacfisf  20866  chfacfisfcpmat  20867  chfacfscmulfsupp  20871  chfacfpmmulfsupp  20875  chfacfpmmulgsum2  20877  2ndcctbss  21466  finlocfin  21531  dissnlocfin  21540  locfindis  21541  locfincf  21542  isfild  21869  infil  21874  neifil  21891  flimfcls  22037  istgp2  22102  oppgtmd  22108  oppgtgp  22109  distgp  22110  indistgp  22111  symgtgp  22112  submtmd  22115  subgtgp  22116  qustgplem  22131  prdstmdd  22134  prdstgpd  22135  tlmtgp  22206  isngp4  22623  subgngp  22646  ngptgp  22647  tngngp2  22663  nrgtrg  22701  nrgtdrg  22704  elii2  22942  icopnfcnv  22948  xrhmeo  22952  lebnumii  22972  phtpcer  23001  reparpht  23004  phtpcco2  23005  pcohtpy  23026  pcoass  23030  pcorevlem  23032  isclmi  23083  isncvsngpd  23156  cphsubrglem  23183  cphclm  23195  tchclm  23237  tchcph  23242  clsocv  23255  pjthlem2  23415  ovolf  23457  iundisj2  23524  vitalilem2  23584  vitali  23588  itg2monolem3  23727  dvfsumlem1  23997  dvfsumlem3  23999  mon1puc1p  24118  uc1pmon1p  24119  ply1remlem  24130  drnguc1p  24138  plyaddlem1  24177  coeidlem  24201  aannenlem2  24292  radcnvcl  24379  pilem2  24414  coseq00topi  24463  coseq0negpitopi  24464  tangtx  24466  tanabsge  24467  cosq14gt0  24471  cosq14ge0  24472  cosordlem  24486  sinord  24489  resinf1o  24491  tanord1  24492  tanord  24493  efif1olem3  24499  efsubm  24506  relogrn  24516  logimclad  24527  logrnaddcl  24529  logneg  24542  logcj  24560  argregt0  24564  argrege0  24565  argimgt0  24566  argimlt0  24567  logimul  24568  logneg2  24569  logdmnrp  24595  logcnlem4  24599  dvloglem  24602  logf1o2  24604  efopnlem2  24611  cxpsqrtlem  24656  relogbval  24718  nnlogbexp  24727  relogbcxp  24731  relogbcxpb  24733  asinneg  24821  asinsin  24827  acoscos  24828  acosbnd  24835  atancj  24845  atanlogaddlem  24848  atanlogsublem  24850  atanlogsub  24851  atantan  24858  atanbndlem  24860  atans2  24866  leibpi  24877  scvxcvx  24920  jensenlem2  24922  emcllem7  24936  basellem1  25015  ppisval  25038  chtdif  25092  ppidif  25097  ppiub  25137  chtublem  25144  chtub  25145  lgsdilem2  25266  gausslemma2dlem1a  25298  gausslemma2dlem2  25300  gausslemma2dlem5  25304  gausslemma2dlem6  25305  lgsquadlem1  25313  lgsquadlem2  25314  lgsquadlem3  25315  2lgslem1  25327  2sqlem3  25353  chebbnd1lem1  25366  chebbnd1lem2  25367  chebbnd1lem3  25368  dchrisumlem2  25387  dchrvmasumlem2  25395  dchrvmasumiflem1  25398  dchrisum0flblem2  25406  mulog2sumlem2  25432  logdivbnd  25453  pntpbnd2  25484  pntibndlem1  25486  pntibnd  25490  pntlemc  25492  pntlemg  25495  pntlemq  25498  pntlemf  25502  padicabvf  25528  padicabvcxp  25529  ostth2  25534  ttgcontlem1  25973  axpaschlem  26028  nbgr2vtx1edg  26456  nbuhgr2vtx1edgb  26458  cusgrexi  26561  structtocusgr  26564  pthdadjvtx  26848  pthdlem1  26884  pthd  26887  crctcshwlkn0lem3  26927  crctcshwlkn0lem4  26928  crctcshwlkn0lem5  26929  crctcshwlkn0lem7  26931  wlkiswwlks1  26988  wwlksm1edg  27002  wwlksnred  27023  wwlksnredwwlkn  27026  wwlksnextproplem3  27043  clwlkclwwlklem2fv1  27132  clwlkclwwlklem2fv2  27133  clwlkclwwlklem2a  27135  clwlkclwwlklem2  27137  clwwisshclwwslemlem  27150  clwwisshclwwslem  27151  erclwwlkref  27157  clwwlkel  27189  clwwlkf  27190  wwlksext2clwwlk  27201  wwlksext2clwwlkOLD  27202  wwlksubclwwlk  27203  umgr2cwwkdifex  27210  clwlksfclwwlkOLD  27230  1pthd  27310  eucrctshift  27410  dlwwlknonclwlknonf1olem1  27538  numclwlk2lem2f  27551  numclwlk2lem2fOLD  27558  frgrreggt1  27575  grpoinvf  27709  strlem3a  29433  hstrlem3a  29441  iundisj2f  29722  fcoinver  29737  ssnnssfz  29870  bcm1n  29875  iundisj2fi  29877  fsumrp0cl  30014  submomnd  30029  lmodslmd  30076  suborng  30134  locfinreflem  30226  locfinref  30227  xrge0iifcnv  30298  xrge0iifiso  30300  xrge0iifhom  30302  esumc  30432  esumle  30439  esumlef  30443  esumpinfsum  30458  esumpcvgval  30459  fiunelros  30556  voliune  30611  volfiniune  30612  sibfinima  30720  eulerpartlemt  30752  fiblem  30779  fibp1  30782  dstrvprob  30852  ballotlemsel1i  30893  ballotlemfrceq  30909  plymulx0  30943  signstfvc  30970  signstfveq0  30973  bnj944  31325  bnj998  31343  bnj1136  31382  bnj1408  31421  erdszelem4  31493  erdszelem8  31497  txsconnlem  31539  cvxsconn  31542  cvmliftpht  31617  snmlff  31628  elmrsubrn  31734  msrf  31756  mthmpps  31796  sinccvglem  31882  noextend  32134  noextendseq  32135  nosupno  32164  trer  32625  poimirlem6  33722  poimirlem7  33723  poimirlem9  33725  poimirlem17  33733  poimirlem20  33736  poimirlem28  33744  poimirlem29  33745  poimirlem30  33746  poimirlem31  33747  poimirlem32  33748  areacirc  33811  nnubfi  33851  prter1  34652  lkrlss  34869  diaf11N  36824  dibf11N  36936  lclkr  37308  lclkrs  37314  lcfrlem9  37325  lcfr  37360  mapd1o  37423  hdmapf1oN  37640  hgmapf1oN  37678  nacsfix  37771  eldioph2lem1  37819  irrapxlem1  37882  rmxypairf1o  37971  jm2.27a  38067  hbtlem2  38189  hbt  38195  cntzsdrg  38267  mon1pid  38278  mon1psubm  38279  binomcxplemnotnn0  39049  elfzfzo  39964  monoords  39986  elfzod  40097  eluzd  40108  fmul01lt1lem2  40291  sumnnodd  40336  ioodvbdlimc1lem2  40621  ioodvbdlimc2lem  40623  iblsplit  40655  iblspltprt  40662  itgspltprt  40668  stoweidlem11  40701  stoweidlem17  40707  fourierdlem12  40809  fourierdlem20  40817  fourierdlem25  40822  fourierdlem37  40834  fourierdlem41  40838  fourierdlem48  40844  fourierdlem49  40845  fourierdlem50  40846  fourierdlem54  40850  fourierdlem64  40860  fourierdlem73  40869  fourierdlem79  40875  fourierdlem102  40898  fourierdlem111  40907  fourierdlem114  40910  etransclem23  40947  etransclem48  40972  2elfz2melfz  41897  elfzlble  41899  fzoopth  41906  iccpartiltu  41927  iccpartigtl  41928  iccpartlt  41929  iccpartgt  41932  lswn0  41949  pfxtrcfv0  41971  pfxeq  41973  pfxtrcfvl  41974  pfx2  41981  pfxccat3  41995  pfxccat3a  41998  fmtnoge3  42011  fmtnodvds  42025  odz2prm2pw  42044  fmtnole4prm  42059  lighneallem4b  42095  mogoldbb  42242  nnsum4primesevenALTV  42258  bgoldbtbndlem3  42264  ringrng  42441  isringrng  42443  lidlrng  42489  ssnn0ssfz  42689  lmod1  42843  elfzolborelfzop1  42871  nnolog2flm1  42946
  Copyright terms: Public domain W3C validator