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

Theorem syl3anbrc 1340
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 1125 . 2 (𝜑 → (𝜓𝜒𝜃))
5 syl3anbrc.4 . 2 (𝜏 ↔ (𝜓𝜒𝜃))
64, 5sylibr 237 1 (𝜑𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  w3a 1084
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 210  df-an 400  df-3an 1086
This theorem is referenced by:  soisores  7063  limuni3  7551  onfununi  7965  smores2  7978  smoiso  7986  oelimcl  8213  iserd  8302  resixp  8484  undifixp  8485  alephval3  9525  canthwelem  10065  canthwe  10066  r1limwun  10151  wunex2  10153  tskcard  10196  gruina  10233  eluzmn  12242  eluzuzle  12244  uztrn  12253  subeluzsub  12267  nn0pzuz  12297  zsupss  12329  nn0ge2m1nnALT  12334  xov1plusxeqvd  12880  ssfzunsnext  12951  ige2m1fz  12996  0elfz  13003  uzsubfz0  13014  elfzmlbm  13016  difelfzle  13019  difelfznle  13020  fvffz0  13024  elfzolt2b  13048  elfzolt3b  13049  elfzouz2  13051  fzossrbm1  13065  elfzo0  13077  eluzgtdifelfzo  13098  elfzodifsumelfzo  13102  fzonn0p1  13113  fzonn0p1p1  13115  fzo0sn0fzo1  13125  ssfzo12bi  13131  ubmelm1fzo  13132  elfzonelfzo  13138  fzosplitprm1  13146  fzostep1  13152  fvinim0ffz  13155  flword2  13182  uzsup  13230  modfzo0difsn  13310  modsumfzodifsn  13311  fsuppmapnn0fiub  13358  suppssfz  13361  1elfz0hash  13751  fzsdom2  13789  ccatrn  13938  ccat2s1fvw  13993  ccat2s1fvwOLD  13994  pfxn0  14043  pfxtrcfv0  14051  pfxtrcfvl  14054  swrdswrd  14062  swrdccatin1  14082  pfxccat3  14091  pfxccat3a  14095  repswswrd  14141  cshwidxmod  14160  cshw1  14179  cshwcsh2id  14185  swrds2  14297  pfx2  14304  2swrd2eqwrdeq  14310  ccat2s1fvwALT  14313  ccat2s1fvwALTOLD  14314  rexuzre  14708  limsupgre  14834  rlimclim1  14898  rlimclim  14899  climrlim2  14900  isercolllem1  15017  isercoll  15020  climcndslem1  15200  fallfacval4  15393  tanhbnd  15510  sinbnd2  15531  cosbnd2  15532  rpnnen2lem12  15574  nn0o  15728  bitsfzolem  15777  bitsfzo  15778  bitsmod  15779  bitsfi  15780  bitsinv1lem  15784  bitsinv1  15785  smueqlem  15833  dvdsnprmd  16028  2mulprm  16031  hashgcdlem  16119  prm23lt5  16145  zgz  16263  gznegcl  16265  gzcjcl  16266  gzaddcl  16267  gzmulcl  16268  vdwlem9  16319  prmgaplem3  16383  prmgaplem4  16384  cshwshashlem2  16426  setsstruct2  16517  ismred  16869  isfuncd  17131  homdmcoa  17323  isdrs2  17545  fpwipodrs  17770  ipodrsima  17771  sgrp2rid2ex  18088  subgid  18277  issubg2  18290  subsubg  18298  gaorber  18434  orbsta  18439  pmtrfconj  18590  psgnunilem2  18619  psgnunilem3  18620  psgnunilem4  18621  pgpfi1  18716  subgpgp  18718  pgpssslw  18735  subgslw  18737  sylow2alem2  18739  fislw  18746  sylow3lem3  18750  efgs1  18857  efgsp1  18859  efgsres  18860  efgredleme  18865  efgcpbllemb  18877  lt6abl  19012  telgsumfzs  19106  ablfac1eu  19192  isringd  19335  ringsrg  19339  ring1  19352  prdsringd  19362  subrgsubg  19538  sdrgid  19572  cntzsdrg  19578  subdrgint  19579  sdrgint  19580  islmodd  19637  islssd  19704  islss4  19731  gzrngunit  20161  expmhm  20164  zringunit  20185  prmirredlem  20190  znidomb  20257  isphld  20347  ocvocv  20364  ocvlss  20365  frlmlbs  20490  gsummoncoe1  20937  mp2pm2mplem4  21418  chfacfisf  21463  chfacfisfcpmat  21464  chfacfscmulfsupp  21468  chfacfpmmulfsupp  21472  chfacfpmmulgsum2  21474  2ndcctbss  22064  finlocfin  22129  dissnlocfin  22138  locfindis  22139  locfincf  22140  isfild  22467  infil  22472  neifil  22489  flimfcls  22635  istgp2  22700  oppgtmd  22706  oppgtgp  22707  distgp  22708  indistgp  22709  efmndtmd  22710  submtmd  22713  subgtgp  22714  symgtgp  22715  qustgplem  22730  prdstmdd  22733  prdstgpd  22734  tlmtgp  22805  isngp4  23222  subgngp  23245  ngptgp  23246  tngngp2  23262  nrgtrg  23300  nrgtdrg  23303  elii2  23545  icopnfcnv  23551  xrhmeo  23555  lebnumii  23575  phtpcer  23604  reparpht  23607  phtpcco2  23608  pcohtpy  23629  pcoass  23633  pcorevlem  23635  isclmi  23686  isncvsngpd  23759  cphsubrglem  23786  cphclm  23798  phclm  23840  tcphcph  23845  clsocv  23858  cphsscph  23859  cmslssbn  23980  pjthlem2  24046  ovolf  24090  iundisj2  24157  vitalilem2  24217  vitali  24221  itg2monolem3  24360  dvfsumlem1  24633  dvfsumlem3  24635  mon1puc1p  24755  uc1pmon1p  24756  ply1remlem  24767  drnguc1p  24775  plyaddlem1  24814  coeidlem  24838  aannenlem2  24929  radcnvcl  25016  pilem2  25051  coseq00topi  25099  coseq0negpitopi  25100  tangtx  25102  tanabsge  25103  cosq14gt0  25107  cosq14ge0  25108  cosq34lt1  25123  cosordlem  25126  cos0pilt1  25128  sinord  25130  resinf1o  25132  tanord1  25133  tanord  25134  efif1olem3  25140  efsubm  25147  relogrn  25157  logimclad  25168  logrnaddcl  25170  logneg  25183  logcj  25201  argregt0  25205  argrege0  25206  argimgt0  25207  argimlt0  25208  logimul  25209  logneg2  25210  logdmnrp  25236  logcnlem4  25240  dvloglem  25243  logf1o2  25245  efopnlem2  25252  cxpsqrtlem  25297  relogbval  25362  nnlogbexp  25371  relogbcxp  25375  relogbcxpb  25377  logbgt0b  25383  asinneg  25476  asinsin  25482  acoscos  25483  acosbnd  25490  atancj  25500  atanlogaddlem  25503  atanlogsublem  25505  atanlogsub  25506  atantan  25513  atanbndlem  25515  atans2  25521  leibpi  25532  scvxcvx  25575  jensenlem2  25577  emcllem7  25591  basellem1  25670  ppisval  25693  chtdif  25747  ppidif  25752  ppiub  25792  chtublem  25799  chtub  25800  lgsdilem2  25921  gausslemma2dlem1a  25953  gausslemma2dlem2  25955  gausslemma2dlem5  25959  gausslemma2dlem6  25960  lgsquadlem1  25968  lgsquadlem2  25969  lgsquadlem3  25970  2lgslem1  25982  2sqlem3  26008  chebbnd1lem1  26057  chebbnd1lem2  26058  chebbnd1lem3  26059  dchrisumlem2  26078  dchrvmasumlem2  26086  dchrvmasumiflem1  26089  dchrisum0flblem2  26097  mulog2sumlem2  26123  logdivbnd  26144  pntpbnd2  26175  pntibndlem1  26177  pntibnd  26181  pntlemc  26183  pntlemg  26186  pntlemq  26189  pntlemf  26193  padicabvf  26219  padicabvcxp  26220  ostth2  26225  ttgcontlem1  26683  axpaschlem  26738  nbgr2vtx1edg  27144  nbuhgr2vtx1edgb  27146  cusgrexi  27237  structtocusgr  27240  pthdadjvtx  27523  pthdlem1  27559  pthd  27562  crctcshwlkn0lem3  27602  crctcshwlkn0lem4  27603  crctcshwlkn0lem5  27604  crctcshwlkn0lem7  27606  wlkiswwlks1  27657  wwlksm1edg  27671  wwlksnred  27682  wwlksnredwwlkn  27685  wwlksnextproplem3  27701  clwlkclwwlklem2fv1  27784  clwlkclwwlklem2fv2  27785  clwlkclwwlklem2a  27787  clwlkclwwlklem2  27789  clwwisshclwwslemlem  27802  clwwisshclwwslem  27803  erclwwlkref  27809  clwwlkel  27835  clwwlkf  27836  wwlksext2clwwlk  27846  wwlksubclwwlk  27847  umgr2cwwkdifex  27854  1pthd  27932  eucrctshift  28032  dlwwlknondlwlknonf1olem1  28153  numclwlk2lem2f  28166  frgrreggt1  28182  grpoinvf  28319  strlem3a  30039  hstrlem3a  30047  iundisj2f  30357  fcoinver  30374  fresf1o  30394  ssnnssfz  30540  bcm1n  30548  iundisj2fi  30550  fsumrp0cl  30733  submomnd  30765  cycpmco2lem6  30827  lmodslmd  30886  suborng  30943  intlidl  31014  rhmpreimaidl  31015  idlinsubrg  31020  rhmimaidl  31021  ssmxidllem  31053  locfinreflem  31197  locfinref  31198  xrge0iifcnv  31290  xrge0iifiso  31292  xrge0iifhom  31294  esumc  31424  esumle  31431  esumlef  31435  esumpinfsum  31450  esumpcvgval  31451  fiunelros  31547  voliune  31602  volfiniune  31603  sibfinima  31711  eulerpartlemt  31743  fiblem  31770  fibp1  31773  dstrvprob  31843  ballotlemsel1i  31884  ballotlemfrceq  31900  plymulx0  31931  signstfvc  31958  signstfveq0  31961  bnj944  32324  bnj998  32343  bnj1136  32383  bnj1408  32422  erdszelem4  32555  erdszelem8  32559  txsconnlem  32601  cvxsconn  32604  cvmliftpht  32679  snmlff  32690  elmrsubrn  32881  msrf  32903  mthmpps  32943  sinccvglem  33029  noextend  33287  noextendseq  33288  nosupno  33317  trer  33778  poimirlem6  35062  poimirlem7  35063  poimirlem9  35065  poimirlem17  35073  poimirlem20  35076  poimirlem28  35084  poimirlem29  35085  poimirlem30  35086  poimirlem31  35087  poimirlem32  35088  areacirc  35149  nnubfi  35187  prter1  36174  lkrlss  36390  diaf11N  38344  dibf11N  38456  lclkr  38828  lclkrs  38834  lcfrlem9  38845  lcfr  38880  mapd1o  38943  hdmapf1oN  39160  hgmapf1oN  39198  frlmvscadiccat  39437  sn-inelr  39587  nacsfix  39650  eldioph2lem1  39698  irrapxlem1  39760  rmxypairf1o  39849  jm2.27a  39943  hbtlem2  40065  hbt  40071  mon1pid  40146  mon1psubm  40147  pren2d  40252  binomcxplemnotnn0  41057  elixpconstg  41722  elfzfzo  41904  monoords  41926  elfzod  42034  eluzd  42043  fmul01lt1lem2  42224  sumnnodd  42269  ioodvbdlimc1lem2  42571  ioodvbdlimc2lem  42573  iblsplit  42605  iblspltprt  42612  itgspltprt  42618  stoweidlem11  42650  stoweidlem17  42656  fourierdlem12  42758  fourierdlem20  42766  fourierdlem25  42771  fourierdlem37  42783  fourierdlem41  42787  fourierdlem48  42793  fourierdlem49  42794  fourierdlem50  42795  fourierdlem54  42799  fourierdlem64  42809  fourierdlem73  42818  fourierdlem79  42824  fourierdlem102  42847  fourierdlem111  42856  fourierdlem114  42859  etransclem23  42896  etransclem48  42921  2elfz2melfz  43872  elfzlble  43874  fzoopth  43881  iccpartiltu  43936  iccpartigtl  43937  iccpartlt  43938  iccpartgt  43941  lswn0  43958  fmtnoge3  44044  fmtnodvds  44058  odz2prm2pw  44077  fmtnole4prm  44092  lighneallem4b  44124  mogoldbb  44300  nnsum4primesevenALTV  44316  bgoldbtbndlem3  44322  ringrng  44500  isringrng  44502  lidlrng  44548  ssnn0ssfz  44748  lmod1  44898  elfzolborelfzop1  44925  nnolog2flm1  45001
  Copyright terms: Public domain W3C validator