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

Theorem syl3anbrc 1238
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 1234 . 2 (𝜑 → (𝜓𝜒𝜃))
5 syl3anbrc.4 . 2 (𝜏 ↔ (𝜓𝜒𝜃))
64, 5sylibr 222 1 (𝜑𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  w3a 1030
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 195  df-an 384  df-3an 1032
This theorem is referenced by:  soisores  6454  limuni3  6921  onfununi  7302  smores2  7315  smoiso  7323  oelimcl  7544  iserd  7632  erinxp  7685  resixp  7806  undifixp  7807  alephval3  8793  fpwwe2lem12  9319  canthwelem  9328  canthwe  9329  r1limwun  9414  wunex2  9416  tskcard  9459  gruina  9496  nqerf  9608  nqerid  9611  eluzmn  11528  eluzuzle  11530  uztrn  11538  nn0pzuz  11579  zsupss  11611  nn0ge2m1nnALT  11616  xov1plusxeqvd  12147  ssfzunsn  12214  ige2m1fz  12256  0elfz  12262  uzsubfz0  12273  elfzmlbm  12275  difelfzle  12278  difelfznle  12279  fvffz0  12283  elfzolt2b  12307  elfzolt3b  12308  elfzouz2  12310  fzossrbm1  12323  elfzo0  12333  eluzgtdifelfzo  12354  elfzodifsumelfzo  12358  fzonn0p1  12368  fzonn0p1p1  12370  elfzom1p1elfzo  12371  fzo0sn0fzo1  12381  ssfzo12bi  12386  ubmelm1fzo  12387  elfzonelfzo  12393  fzosplitprm1  12400  fzostep1  12403  fvinim0ffz  12406  flword2  12433  uzsup  12481  modfzo0difsn  12561  modsumfzodifsn  12562  fsuppmapnn0fiub  12609  fsuppmapnn0fiubOLD  12610  suppssfz  12613  1elfz0hash  12994  fzsdom2  13029  ccatrn  13173  swrdn0  13230  swrdtrcfv  13241  swrdtrcfv0  13242  swrdeq  13244  swrdtrcfvl  13250  swrdswrd  13260  swrdccatwrd  13268  wrdeqs1cat  13274  swrdccatin1  13282  swrdccat3  13291  swrdccatid  13296  repswswrd  13330  cshwidxmod  13348  cshw1  13367  cshwcsh2id  13373  swrds2  13481  2swrd2eqwrdeq  13492  ccat2s1fvwALT  13494  rexuzre  13888  limsupgre  14008  rlimclim1  14072  rlimclim  14073  climrlim2  14074  isercolllem1  14191  isercoll  14194  climcndslem1  14368  fallfacval4  14561  tanhbnd  14678  sinbnd2  14699  cosbnd2  14700  rpnnen2lem12  14741  nn0o  14885  bitsfzolem  14942  bitsfzo  14943  bitsmod  14944  bitsfi  14945  bitsinv1lem  14949  bitsinv1  14950  smueqlem  14998  dvdsnprmd  15189  hashgcdlem  15279  prm23lt5  15305  zgz  15423  gznegcl  15425  gzcjcl  15426  gzaddcl  15427  gzmulcl  15428  vdwlem9  15479  prmgaplem3  15543  prmgaplem4  15544  cshwshashlem2  15589  ismred  16033  isfuncd  16296  homdmcoa  16488  isdrs2  16710  fpwipodrs  16935  ipodrsima  16936  psss  16985  psssdm2  16986  sgrp2rid2ex  17185  subgid  17367  issubg2  17380  subsubg  17388  gaorber  17512  orbsta  17517  pmtrfconj  17657  psgnunilem2  17686  psgnunilem3  17687  psgnunilem4  17688  pgpfi1  17781  subgpgp  17783  pgpssslw  17800  subgslw  17802  sylow2alem2  17804  fislw  17811  sylow3lem3  17815  efgs1  17919  efgsp1  17921  efgsres  17922  efgredleme  17927  efgcpbllemb  17939  lt6abl  18067  telgsumfzs  18157  ablfac1eu  18243  isringd  18356  ringsrg  18360  ring1  18373  prdsringd  18383  subrgsubg  18557  islmodd  18640  islssd  18705  islss4  18731  gsummoncoe1  19443  gzrngunit  19579  expmhm  19582  zringunit  19605  prmirredlem  19607  znidomb  19676  isphld  19765  ocvocv  19781  ocvlss  19782  frlmlbs  19902  mp2pm2mplem4  20380  chfacfisf  20425  chfacfisfcpmat  20426  chfacfscmulfsupp  20430  chfacfpmmulfsupp  20434  chfacfpmmulgsum2  20436  2ndcctbss  21015  finlocfin  21080  dissnlocfin  21089  locfindis  21090  locfincf  21091  isfild  21419  infil  21424  neifil  21441  flimfcls  21587  istgp2  21652  oppgtmd  21658  oppgtgp  21659  distgp  21660  indistgp  21661  symgtgp  21662  submtmd  21665  subgtgp  21666  qustgplem  21681  prdstmdd  21684  prdstgpd  21685  tlmtgp  21756  isngp4  22173  subgngp  22196  ngptgp  22197  tngngp2  22213  nrgtrg  22251  nrgtdrg  22254  elii2  22490  icopnfcnv  22496  xrhmeo  22500  lebnumii  22520  phtpcer  22549  phtpcerOLD  22550  reparpht  22553  phtpcco2  22554  pcohtpy  22575  pcoass  22579  pcorevlem  22581  pi1cpbl  22599  pi1grplem  22604  isclmi  22632  isncvsngpd  22702  cphsubrglem  22729  cphclm  22741  tchclm  22783  tchcph  22788  clsocv  22801  pjthlem2  22961  ovolf  23001  iundisj2  23068  vitalilem2  23128  vitali  23132  itg2monolem3  23269  dvfsumlem1  23537  dvfsumlem3  23539  mon1puc1p  23658  uc1pmon1p  23659  ply1remlem  23670  drnguc1p  23678  plyaddlem1  23717  coeidlem  23741  aannenlem2  23832  radcnvcl  23919  pilem2  23954  coseq00topi  24002  coseq0negpitopi  24003  tangtx  24005  tanabsge  24006  cosq14gt0  24010  cosq14ge0  24011  cosordlem  24025  sinord  24028  resinf1o  24030  tanord1  24031  tanord  24032  efif1olem3  24038  efsubm  24045  relogrn  24056  logimclad  24067  logrnaddcl  24069  logneg  24082  logcj  24100  argregt0  24104  argrege0  24105  argimgt0  24106  argimlt0  24107  logimul  24108  logneg2  24109  logdmnrp  24131  logcnlem4  24135  dvloglem  24138  logf1o2  24140  efopnlem2  24147  cxpsqrtlem  24192  relogbval  24254  nnlogbexp  24263  relogbcxp  24267  relogbcxpb  24269  asinneg  24357  asinsin  24363  acoscos  24364  acosbnd  24371  atancj  24381  atanlogaddlem  24384  atanlogsublem  24386  atanlogsub  24387  atantan  24394  atanbndlem  24396  atans2  24402  leibpi  24413  scvxcvx  24456  jensenlem2  24458  emcllem7  24472  basellem1  24551  ppisval  24574  chtdif  24628  ppidif  24633  ppiub  24673  chtublem  24680  chtub  24681  lgsdilem2  24802  gausslemma2dlem1a  24834  gausslemma2dlem2  24836  gausslemma2dlem5  24840  gausslemma2dlem6  24841  lgsquadlem1  24849  lgsquadlem2  24850  lgsquadlem3  24851  2lgslem1  24863  2sqlem3  24889  chebbnd1lem1  24902  chebbnd1lem2  24903  chebbnd1lem3  24904  dchrisumlem2  24923  dchrvmasumlem2  24931  dchrvmasumiflem1  24934  dchrisum0flblem2  24942  mulog2sumlem2  24968  logdivbnd  24989  pntpbnd2  25020  pntibndlem1  25022  pntibnd  25026  pntlemc  25028  pntlemg  25031  pntlemq  25034  pntlemf  25038  padicabvf  25064  padicabvcxp  25065  ostth2  25070  ttgcontlem1  25510  axpaschlem  25565  nbgraf1olem5  25767  cyclnspth  25952  wwlknred  26044  wwlknredwwlkn  26047  wwlkextproplem3  26064  clwlkisclwwlklem2fv1  26103  clwlkisclwwlklem2fv2  26104  clwlkisclwwlklem2a  26106  clwlkisclwwlklem1  26108  clwwlkel  26114  clwwlkf  26115  wwlkext2clwwlk  26124  clwwisshclwwlem1  26126  clwwisshclwwlem  26127  erclwwlkref  26134  usg2cwwkdifex  26142  clwlkfclwwlk1hash  26162  clwlkfclwwlk  26164  eupath2lem3  26299  extwwlkfablem2  26398  numclwlk2lem2f  26423  frgrareggt1  26436  grpoinvf  26563  strlem3a  28288  hstrlem3a  28296  iundisj2f  28578  fcoinver  28591  ssnnssfz  28730  bcm1n  28734  iundisj2fi  28736  fsumrp0cl  28819  submomnd  28834  lmodslmd  28881  suborng  28939  locfinreflem  29028  locfinref  29029  xrge0iifcnv  29100  xrge0iifiso  29102  xrge0iifhom  29104  esumc  29233  esumle  29240  esumlef  29244  esumpinfsum  29259  esumpcvgval  29260  fiunelros  29357  voliune  29412  volfiniune  29413  sibfinima  29521  eulerpartlemt  29553  fiblem  29580  fibp1  29583  dstrvprob  29653  ballotlemsel1i  29694  ballotlemfrceq  29710  plymulx0  29743  signstfvc  29770  signstfveq0  29773  bnj944  30055  bnj998  30073  bnj1136  30112  bnj1408  30151  erdszelem4  30223  erdszelem8  30227  txsconlem  30269  cvxscon  30272  cvmliftpht  30347  snmlff  30358  elmrsubrn  30464  msrf  30486  mthmpps  30526  sinccvglem  30613  trer  31273  poimirlem6  32368  poimirlem7  32369  poimirlem9  32371  poimirlem17  32379  poimirlem20  32382  poimirlem28  32390  poimirlem29  32391  poimirlem30  32392  poimirlem31  32393  poimirlem32  32394  areacirc  32458  nnubfi  32499  prter1  32965  lkrlss  33183  diaf11N  35139  dibf11N  35251  lclkr  35623  lclkrs  35629  lcfrlem9  35640  lcfr  35675  mapd1o  35738  hdmapf1oN  35958  hgmapf1oN  35996  nacsfix  36076  eldioph2lem1  36124  irrapxlem1  36187  rmxypairf1o  36277  jm2.27a  36373  hbtlem2  36496  hbt  36502  cntzsdrg  36574  mon1pid  36585  mon1psubm  36586  binomcxplemnotnn0  37360  elfzfzo  38212  monoords  38235  fmul01lt1lem2  38435  sumnnodd  38480  ioodvbdlimc1lem2  38605  ioodvbdlimc2lem  38607  iblsplit  38641  iblspltprt  38648  itgspltprt  38654  stoweidlem11  38687  stoweidlem17  38693  fourierdlem12  38795  fourierdlem20  38803  fourierdlem25  38808  fourierdlem37  38820  fourierdlem41  38824  fourierdlem48  38830  fourierdlem49  38831  fourierdlem50  38832  fourierdlem54  38836  fourierdlem64  38846  fourierdlem73  38855  fourierdlem79  38861  fourierdlem102  38884  fourierdlem111  38893  fourierdlem114  38896  etransclem23  38933  etransclem48  38958  iccpartiltu  39744  iccpartigtl  39745  iccpartlt  39746  iccpartgt  39749  fmtnoge3  39764  fmtnodvds  39778  odz2prm2pw  39797  fmtnole4prm  39812  lighneallem4b  39848  nnsum4primesevenALTV  40001  bgoldbtbndlem3  40007  lswn0  40026  pfxtrcfv0  40049  pfxeq  40051  pfxtrcfvl  40052  pfx2  40059  pfxccat3  40073  pfxccat3a  40076  2elfz2melfz  40161  elfzlble  40163  fzoopth  40166  structvtxvallem  40234  pthdadjvtx  40917  pthdlem1  40953  crctcsh1wlkn0lem3  40996  crctcsh1wlkn0lem4  40997  crctcsh1wlkn0lem5  40998  crctcsh1wlkn0lem7  41000  1wlkiswwlks1  41045  wwlksm1edg  41059  wwlksnred  41079  wwlksnredwwlkn  41082  wwlksnextproplem3  41098  clwlkclwwlklem2fv1  41185  clwlkclwwlklem2fv2  41186  clwlkclwwlklem2a  41188  clwlkclwwlklem2  41190  clwwlksel  41202  clwwlksf  41203  wwlksext2clwwlk  41212  wwlksubclwwlks  41213  clwwisshclwwslemlem  41214  clwwisshclwwslem  41215  erclwwlksref  41222  umgr2cwwkdifex  41230  clwlksfclwwlk  41250  eucrctshift  41392  av-extwwlkfablem2  41491  av-numclwlk2lem2f  41514  av-frgrareggt1  41528  ringrng  41650  isringrng  41652  lidlrng  41698  ssnn0ssfz  41901  lmod1  42056  elfzolborelfzop1  42084  nnolog2flm1  42163
  Copyright terms: Public domain W3C validator