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

Step	Hyp	Ref	Expression
1		syl3anbrc.1	. . 3 ⊢ (𝜑 → 𝜓)
2		syl3anbrc.2	. . 3 ⊢ (𝜑 → 𝜒)
3		syl3anbrc.3	. . 3 ⊢ (𝜑 → 𝜃)
4	1, 2, 3	3jca 1128	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
5		syl3anbrc.4	. 2 ⊢ (𝜏 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))
6	4, 5	sylibr 234	1 ⊢ (𝜑 → 𝜏)

Syntax hints:   → wi 4   ↔ wb 206   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  soisores  7302  limuni3  7828  onfununi  8310  smores2  8323  smoiso  8331  oelimcl  8564  iserd  8697  resixp  8906  undifixp  8907  alephval3  10063  canthwelem  10603  canthwe  10604  r1limwun  10689  wunex2  10691  tskcard  10734  gruina  10771  eluzmn  12800  eluzuzle  12802  uztrn  12811  eluzadd  12822  eluzsub  12823  subeluzsub  12830  nn0pzuz  12864  zsupss  12896  nn0ge2m1nnALT  12901  xov1plusxeqvd  13459  ige2m1fz  13578  0elfz  13585  uzsubfz0  13597  elfzmlbm  13599  difelfzle  13602  difelfznle  13603  fvffz0  13607  elfzolt2b  13631  elfzolt3b  13632  elfzouz2  13635  fzossrbm1  13649  elfzo0  13661  eluzgtdifelfzo  13688  elfzodifsumelfzo  13692  fzonn0p1  13703  fzonn0p1p1  13705  fzo0sn0fzo1  13716  ssfzo12bi  13722  fzoopth  13723  ubmelm1fzo  13724  elfzonelfzo  13730  fzosplitprm1  13738  fzostep1  13744  fvinim0ffz  13747  flword2  13775  uzsup  13825  modfzo0difsn  13908  modsumfzodifsn  13909  fsuppmapnn0fiub  13956  suppssfz  13959  1elfz0hash  14355  fzsdom2  14393  ccatrn  14554  ccat2s1fvw  14603  pfxn0  14651  pfxtrcfv0  14659  pfxtrcfvl  14662  swrdswrd  14670  swrdccatin1  14690  pfxccat3  14699  pfxccat3a  14703  repswswrd  14749  cshwidxmod  14768  cshw1  14787  cshwcsh2id  14794  swrds2  14906  pfx2  14913  2swrd2eqwrdeq  14919  ccat2s1fvwALT  14921  rexuzre  15319  limsupgre  15447  rlimclim1  15511  rlimclim  15512  climrlim2  15513  isercolllem1  15631  isercoll  15634  climcndslem1  15815  fallfacval4  16009  tanhbnd  16129  sinbnd2  16150  cosbnd2  16151  rpnnen2lem12  16193  nn0o  16353  bitsfzolem  16404  bitsfzo  16405  bitsmod  16406  bitsfi  16407  bitsinv1lem  16411  bitsinv1  16412  smueqlem  16460  dvdsnprmd  16660  2mulprm  16663  hashgcdlem  16758  prm23lt5  16785  zgz  16904  gznegcl  16906  gzcjcl  16907  gzaddcl  16908  gzmulcl  16909  vdwlem9  16960  prmgaplem3  17024  prmgaplem4  17025  cshwshashlem2  17067  setsstruct2  17144  ismred  17563  isfuncd  17827  homdmcoa  18029  isdrs2  18267  fpwipodrs  18499  ipodrsima  18500  sgrp2rid2ex  18854  subgid  19060  issubg2  19073  subsubg  19081  gaorber  19240  orbsta  19245  pmtrfconj  19396  psgnunilem2  19425  psgnunilem3  19426  psgnunilem4  19427  pgpfi1  19525  subgpgp  19527  pgpssslw  19544  subgslw  19546  sylow2alem2  19548  fislw  19555  sylow3lem3  19559  efgs1  19665  efgsp1  19667  efgsres  19668  efgredleme  19673  efgcpbllemb  19685  lt6abl  19825  telgsumfzs  19919  ablfac1eu  20005  isrngd  20082  prdsrngd  20085  ringrng  20194  isringrng  20196  isringd  20200  ringsrg  20206  ring1  20219  prdsringd  20230  subrngid  20458  subrngsubg  20461  issubrng2  20467  subsubrng  20472  subrgsubg  20486  subrgsubrng  20487  sdrgid  20701  cntzsdrg  20711  subdrgint  20712  sdrgint  20713  islmodd  20772  islssd  20841  islss4  20868  dflidl2rng  21128  rnglidl0  21139  rnglidl1  21142  rnglidlrng  21157  rng2idlsubrng  21175  rhmpreimaidl  21187  gzrngunit  21350  expmhm  21353  zringunit  21376  prmirredlem  21382  znidomb  21471  isphld  21563  ocvocv  21580  ocvlss  21581  frlmlbs  21706  psdmul  22053  gsummoncoe1  22195  mp2pm2mplem4  22696  chfacfisf  22741  chfacfisfcpmat  22742  chfacfscmulfsupp  22746  chfacfpmmulfsupp  22750  chfacfpmmulgsum2  22752  2ndcctbss  23342  finlocfin  23407  dissnlocfin  23416  locfindis  23417  locfincf  23418  isfild  23745  infil  23750  neifil  23767  flimfcls  23913  istgp2  23978  oppgtmd  23984  oppgtgp  23985  distgp  23986  indistgp  23987  efmndtmd  23988  submtmd  23991  subgtgp  23992  symgtgp  23993  qustgplem  24008  prdstmdd  24011  prdstgpd  24012  tlmtgp  24083  isngp4  24500  subgngp  24523  ngptgp  24524  tngngp2  24540  nrgtrg  24578  nrgtdrg  24581  elii2  24832  icopnfcnv  24840  xrhmeo  24844  lebnumii  24865  phtpcer  24894  reparpht  24898  phtpcco2  24899  pcohtpy  24920  pcoass  24924  pcorevlem  24926  isclmi  24977  isncvsngpd  25050  cphsubrglem  25077  cphclm  25089  phclm  25132  tcphcph  25137  clsocv  25150  cphsscph  25151  cmslssbn  25272  pjthlem2  25338  ovolf  25383  iundisj2  25450  vitalilem2  25510  vitali  25514  itg2monolem3  25653  dvfsumlem1  25932  dvfsumlem3  25935  mon1puc1p  26056  uc1pmon1p  26057  mon1pid  26059  ply1remlem  26070  drnguc1p  26079  plyaddlem1  26118  coeidlem  26142  aannenlem2  26237  radcnvcl  26326  pilem2  26362  coseq00topi  26411  coseq0negpitopi  26412  tangtx  26414  tanabsge  26415  cosq14gt0  26419  cosq14ge0  26420  cosq34lt1  26436  cosordlem  26439  cos0pilt1  26441  sinord  26443  resinf1o  26445  tanord1  26446  tanord  26447  efif1olem3  26453  efsubm  26460  relogrn  26470  logimclad  26481  logrnaddcl  26483  logneg  26497  logcj  26515  argregt0  26519  argrege0  26520  argimgt0  26521  argimlt0  26522  logimul  26523  logneg2  26524  logdmnrp  26550  logcnlem4  26554  dvloglem  26557  logf1o2  26559  efopnlem2  26566  cxpsqrtlem  26611  relogbval  26682  nnlogbexp  26691  relogbcxp  26695  relogbcxpb  26697  logbgt0b  26703  asinneg  26796  asinsin  26802  acoscos  26803  acosbnd  26810  atancj  26820  atanlogaddlem  26823  atanlogsublem  26825  atanlogsub  26826  atantan  26833  atanbndlem  26835  atans2  26841  leibpi  26852  scvxcvx  26896  jensenlem2  26898  emcllem7  26912  basellem1  26991  ppisval  27014  chtdif  27068  ppidif  27073  ppiub  27115  chtublem  27122  chtub  27123  lgsdilem2  27244  gausslemma2dlem1a  27276  gausslemma2dlem2  27278  gausslemma2dlem5  27282  gausslemma2dlem6  27283  lgsquadlem1  27291  lgsquadlem2  27292  lgsquadlem3  27293  2lgslem1  27305  2sqlem3  27331  chebbnd1lem1  27380  chebbnd1lem2  27381  chebbnd1lem3  27382  dchrisumlem2  27401  dchrvmasumlem2  27409  dchrvmasumiflem1  27412  dchrisum0flblem2  27420  mulog2sumlem2  27446  logdivbnd  27467  pntpbnd2  27498  pntibndlem1  27500  pntibnd  27504  pntlemc  27506  pntlemg  27509  pntlemq  27512  pntlemf  27516  padicabvf  27542  padicabvcxp  27543  ostth2  27548  noextend  27578  noextendseq  27579  nosupno  27615  noinfno  27630  ttgcontlem1  28812  axpaschlem  28867  nbgr2vtx1edg  29277  nbuhgr2vtx1edgb  29279  cusgrexi  29370  structtocusgr  29373  pthdadjvtx  29658  pthdlem1  29696  pthd  29699  crctcshwlkn0lem3  29742  crctcshwlkn0lem4  29743  crctcshwlkn0lem5  29744  crctcshwlkn0lem7  29746  wlkiswwlks1  29797  wwlksm1edg  29811  wwlksnred  29822  wwlksnredwwlkn  29825  wwlksnextproplem3  29841  clwlkclwwlklem2fv1  29924  clwlkclwwlklem2fv2  29925  clwlkclwwlklem2a  29927  clwlkclwwlklem2  29929  clwwisshclwwslemlem  29942  clwwisshclwwslem  29943  erclwwlkref  29949  clwwlkel  29975  clwwlkf  29976  wwlksext2clwwlk  29986  wwlksubclwwlk  29987  umgr2cwwkdifex  29994  1pthd  30072  eucrctshift  30172  dlwwlknondlwlknonf1olem1  30293  numclwlk2lem2f  30306  frgrreggt1  30322  grpoinvf  30461  strlem3a  32181  hstrlem3a  32189  iundisj2f  32519  fcoinver  32533  fresf1o  32555  ssnnssfz  32710  bcm1n  32718  iundisj2fi  32720  ccatdmss  32871  chnub  32938  chnso  32940  fsumrp0cl  32962  submomnd  33024  cycpmco2lem6  33088  lmodslmd  33157  fldgensdrg  33264  suborng  33293  intlidl  33391  idlinsubrg  33402  rhmimaidl  33403  ssdifidllem  33427  ssmxidllem  33444  1arithidomlem1  33506  1arithidomlem2  33507  1arithidom  33508  fldextsdrg  33650  fldextrspunlem2  33672  fldextrspundgdvdslem  33675  fldextrspundgdvds  33676  minplyirred  33701  algextdeglem4  33710  algextdeglem8  33714  rtelextdg2lem  33716  constrsdrg  33765  2sqr3minply  33770  cos9thpiminply  33778  locfinreflem  33830  locfinref  33831  xrge0iifcnv  33923  xrge0iifiso  33925  xrge0iifhom  33927  esumc  34041  esumle  34048  esumlef  34052  esumpinfsum  34067  esumpcvgval  34068  fiunelros  34164  voliune  34219  volfiniune  34220  sibfinima  34330  eulerpartlemt  34362  fiblem  34389  fibp1  34392  dstrvprob  34463  ballotlemsel1i  34504  ballotlemfrceq  34520  plymulx0  34538  signstfvc  34565  signstfveq0  34568  bnj944  34928  bnj998  34947  bnj1136  34987  bnj1408  35026  erdszelem4  35181  erdszelem8  35185  txsconnlem  35227  cvxsconn  35230  cvmliftpht  35305  snmlff  35316  elmrsubrn  35507  msrf  35529  mthmpps  35569  sinccvglem  35659  trer  36304  poimirlem6  37620  poimirlem7  37621  poimirlem9  37623  poimirlem17  37631  poimirlem20  37634  poimirlem28  37642  poimirlem29  37643  poimirlem30  37644  poimirlem31  37645  poimirlem32  37646  areacirc  37707  nnubfi  37744  prter1  38872  lkrlss  39088  diaf11N  41043  dibf11N  41155  lclkr  41527  lclkrs  41533  lcfrlem9  41544  lcfr  41579  mapd1o  41642  hdmapf1oN  41859  hgmapf1oN  41897  frlmvscadiccat  42494  fimgmcyc  42522  nacsfix  42700  eldioph2lem1  42748  irrapxlem1  42810  rmxypairf1o  42900  jm2.27a  42994  hbtlem2  43113  hbt  43119  mon1psubm  43188  onnog  43418  pren2d  43545  binomcxplemnotnn0  44345  elixpconstg  45083  elfzfzo  45275  monoords  45295  elfzod  45396  eluzd  45405  fmul01lt1lem2  45583  sumnnodd  45628  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  iblsplit  45964  iblspltprt  45971  itgspltprt  45977  stoweidlem11  46009  stoweidlem17  46015  fourierdlem12  46117  fourierdlem20  46125  fourierdlem25  46130  fourierdlem37  46142  fourierdlem41  46146  fourierdlem48  46152  fourierdlem49  46153  fourierdlem50  46154  fourierdlem54  46158  fourierdlem64  46168  fourierdlem73  46177  fourierdlem79  46183  fourierdlem102  46206  fourierdlem111  46215  fourierdlem114  46218  etransclem23  46255  etransclem48  46280  ormkglobd  46873  2elfz2melfz  47319  elfzlble  47321  ceilhalfelfzo1  47331  1elfzo1ceilhalf1  47338  difltmodne  47343  modm2nep1  47367  modm1nep2  47369  modm1p1ne  47371  iccpartiltu  47423  iccpartigtl  47424  iccpartlt  47425  iccpartgt  47428  lswn0  47445  fmtnoge3  47531  fmtnodvds  47545  odz2prm2pw  47564  fmtnole4prm  47579  lighneallem4b  47610  mogoldbb  47786  nnsum4primesevenALTV  47802  bgoldbtbndlem3  47808  grlimgrtrilem1  47993  gpgprismgriedgdmss  48043  gpgprismgrusgra  48049  gpg3nbgrvtx0  48067  gpg3nbgrvtx0ALT  48068  gpg5nbgrvtx03star  48071  gpg5nbgr3star  48072  gpg3kgrtriexlem3  48076  gpg3kgrtriexlem4  48077  gpg3kgrtriexlem6  48079  gpgprismgr4cycllem3  48087  gpgprismgr4cycllem9  48093  ssnn0ssfz  48337  lmod1  48481  elfzolborelfzop1  48508  nnolog2flm1  48579  funcf2lem2  49071  isnatd  49212