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

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 395  df-3an 1086

This theorem is referenced by:  soisores  7331  limuni3  7854  onfununi  8363  smores2  8376  smoiso  8384  oelimcl  8622  iserd  8752  resixp  8954  undifixp  8955  alephval3  10146  canthwelem  10684  canthwe  10685  r1limwun  10770  wunex2  10772  tskcard  10815  gruina  10852  eluzmn  12875  eluzuzle  12877  uztrn  12886  eluzadd  12897  eluzsub  12898  subeluzsub  12905  nn0pzuz  12935  zsupss  12967  nn0ge2m1nnALT  12972  xov1plusxeqvd  13523  ige2m1fz  13639  0elfz  13646  uzsubfz0  13657  elfzmlbm  13659  difelfzle  13662  difelfznle  13663  fvffz0  13667  elfzolt2b  13691  elfzolt3b  13692  elfzouz2  13695  fzossrbm1  13709  elfzo0  13721  eluzgtdifelfzo  13742  elfzodifsumelfzo  13746  fzonn0p1  13757  fzonn0p1p1  13759  fzo0sn0fzo1  13769  ssfzo12bi  13775  fzoopth  13776  ubmelm1fzo  13777  elfzonelfzo  13783  fzosplitprm1  13791  fzostep1  13797  fvinim0ffz  13800  flword2  13827  uzsup  13877  modfzo0difsn  13957  modsumfzodifsn  13958  fsuppmapnn0fiub  14005  suppssfz  14008  1elfz0hash  14402  fzsdom2  14440  ccatrn  14592  ccat2s1fvw  14641  pfxn0  14689  pfxtrcfv0  14697  pfxtrcfvl  14700  swrdswrd  14708  swrdccatin1  14728  pfxccat3  14737  pfxccat3a  14741  repswswrd  14787  cshwidxmod  14806  cshw1  14825  cshwcsh2id  14832  swrds2  14944  pfx2  14951  2swrd2eqwrdeq  14957  ccat2s1fvwALT  14959  rexuzre  15352  limsupgre  15478  rlimclim1  15542  rlimclim  15543  climrlim2  15544  isercolllem1  15664  isercoll  15667  climcndslem1  15848  fallfacval4  16040  tanhbnd  16158  sinbnd2  16179  cosbnd2  16180  rpnnen2lem12  16222  nn0o  16380  bitsfzolem  16429  bitsfzo  16430  bitsmod  16431  bitsfi  16432  bitsinv1lem  16436  bitsinv1  16437  smueqlem  16485  dvdsnprmd  16686  2mulprm  16689  hashgcdlem  16785  prm23lt5  16811  zgz  16930  gznegcl  16932  gzcjcl  16933  gzaddcl  16934  gzmulcl  16935  vdwlem9  16986  prmgaplem3  17050  prmgaplem4  17051  cshwshashlem2  17094  setsstruct2  17171  ismred  17610  isfuncd  17879  homdmcoa  18084  isdrs2  18326  fpwipodrs  18560  ipodrsima  18561  sgrp2rid2ex  18912  subgid  19118  issubg2  19131  subsubg  19139  gaorber  19298  orbsta  19303  pmtrfconj  19460  psgnunilem2  19489  psgnunilem3  19490  psgnunilem4  19491  pgpfi1  19589  subgpgp  19591  pgpssslw  19608  subgslw  19610  sylow2alem2  19612  fislw  19619  sylow3lem3  19623  efgs1  19729  efgsp1  19731  efgsres  19732  efgredleme  19737  efgcpbllemb  19749  lt6abl  19889  telgsumfzs  19983  ablfac1eu  20069  isrngd  20152  prdsrngd  20155  ringrng  20260  isringrng  20262  isringd  20266  ringsrg  20272  ring1  20285  prdsringd  20296  subrngid  20527  subrngsubg  20530  issubrng2  20536  subsubrng  20541  subrgsubg  20557  subrgsubrng  20558  sdrgid  20767  cntzsdrg  20777  subdrgint  20778  sdrgint  20779  islmodd  20838  islssd  20908  islss4  20935  dflidl2rng  21203  rnglidl0  21214  rnglidl1  21217  rnglidlrng  21232  rng2idlsubrng  21250  rhmpreimaidl  21262  gzrngunit  21426  expmhm  21429  zringunit  21452  prmirredlem  21458  znidomb  21555  isphld  21646  ocvocv  21663  ocvlss  21664  frlmlbs  21791  psdmul  22156  gsummoncoe1  22296  mp2pm2mplem4  22799  chfacfisf  22844  chfacfisfcpmat  22845  chfacfscmulfsupp  22849  chfacfpmmulfsupp  22853  chfacfpmmulgsum2  22855  2ndcctbss  23447  finlocfin  23512  dissnlocfin  23521  locfindis  23522  locfincf  23523  isfild  23850  infil  23855  neifil  23872  flimfcls  24018  istgp2  24083  oppgtmd  24089  oppgtgp  24090  distgp  24091  indistgp  24092  efmndtmd  24093  submtmd  24096  subgtgp  24097  symgtgp  24098  qustgplem  24113  prdstmdd  24116  prdstgpd  24117  tlmtgp  24188  isngp4  24609  subgngp  24632  ngptgp  24633  tngngp2  24657  nrgtrg  24695  nrgtdrg  24698  elii2  24947  icopnfcnv  24955  xrhmeo  24959  lebnumii  24980  phtpcer  25009  reparpht  25013  phtpcco2  25014  pcohtpy  25035  pcoass  25039  pcorevlem  25041  isclmi  25092  isncvsngpd  25166  cphsubrglem  25193  cphclm  25205  phclm  25248  tcphcph  25253  clsocv  25266  cphsscph  25267  cmslssbn  25388  pjthlem2  25454  ovolf  25499  iundisj2  25566  vitalilem2  25626  vitali  25630  itg2monolem3  25770  dvfsumlem1  26048  dvfsumlem3  26051  mon1puc1p  26175  uc1pmon1p  26176  mon1pid  26178  ply1remlem  26189  drnguc1p  26198  plyaddlem1  26237  coeidlem  26261  aannenlem2  26354  radcnvcl  26443  pilem2  26479  coseq00topi  26527  coseq0negpitopi  26528  tangtx  26530  tanabsge  26531  cosq14gt0  26535  cosq14ge0  26536  cosq34lt1  26551  cosordlem  26554  cos0pilt1  26556  sinord  26558  resinf1o  26560  tanord1  26561  tanord  26562  efif1olem3  26568  efsubm  26575  relogrn  26585  logimclad  26596  logrnaddcl  26598  logneg  26612  logcj  26630  argregt0  26634  argrege0  26635  argimgt0  26636  argimlt0  26637  logimul  26638  logneg2  26639  logdmnrp  26665  logcnlem4  26669  dvloglem  26672  logf1o2  26674  efopnlem2  26681  cxpsqrtlem  26726  relogbval  26797  nnlogbexp  26806  relogbcxp  26810  relogbcxpb  26812  logbgt0b  26818  asinneg  26911  asinsin  26917  acoscos  26918  acosbnd  26925  atancj  26935  atanlogaddlem  26938  atanlogsublem  26940  atanlogsub  26941  atantan  26948  atanbndlem  26950  atans2  26956  leibpi  26967  scvxcvx  27011  jensenlem2  27013  emcllem7  27027  basellem1  27106  ppisval  27129  chtdif  27183  ppidif  27188  ppiub  27230  chtublem  27237  chtub  27238  lgsdilem2  27359  gausslemma2dlem1a  27391  gausslemma2dlem2  27393  gausslemma2dlem5  27397  gausslemma2dlem6  27398  lgsquadlem1  27406  lgsquadlem2  27407  lgsquadlem3  27408  2lgslem1  27420  2sqlem3  27446  chebbnd1lem1  27495  chebbnd1lem2  27496  chebbnd1lem3  27497  dchrisumlem2  27516  dchrvmasumlem2  27524  dchrvmasumiflem1  27527  dchrisum0flblem2  27535  mulog2sumlem2  27561  logdivbnd  27582  pntpbnd2  27613  pntibndlem1  27615  pntibnd  27619  pntlemc  27621  pntlemg  27624  pntlemq  27627  pntlemf  27631  padicabvf  27657  padicabvcxp  27658  ostth2  27663  noextend  27693  noextendseq  27694  nosupno  27730  noinfno  27745  ttgcontlem1  28815  axpaschlem  28871  nbgr2vtx1edg  29283  nbuhgr2vtx1edgb  29285  cusgrexi  29376  structtocusgr  29379  pthdadjvtx  29664  pthdlem1  29700  pthd  29703  crctcshwlkn0lem3  29743  crctcshwlkn0lem4  29744  crctcshwlkn0lem5  29745  crctcshwlkn0lem7  29747  wlkiswwlks1  29798  wwlksm1edg  29812  wwlksnred  29823  wwlksnredwwlkn  29826  wwlksnextproplem3  29842  clwlkclwwlklem2fv1  29925  clwlkclwwlklem2fv2  29926  clwlkclwwlklem2a  29928  clwlkclwwlklem2  29930  clwwisshclwwslemlem  29943  clwwisshclwwslem  29944  erclwwlkref  29950  clwwlkel  29976  clwwlkf  29977  wwlksext2clwwlk  29987  wwlksubclwwlk  29988  umgr2cwwkdifex  29995  1pthd  30073  eucrctshift  30173  dlwwlknondlwlknonf1olem1  30294  numclwlk2lem2f  30307  frgrreggt1  30323  grpoinvf  30462  strlem3a  32182  hstrlem3a  32190  iundisj2f  32510  fcoinver  32524  fresf1o  32548  ssnnssfz  32692  bcm1n  32700  iundisj2fi  32702  ccatdmss  32816  chnub  32884  chnso  32886  fsumrp0cl  32907  submomnd  32949  cycpmco2lem6  33013  lmodslmd  33072  fldgensdrg  33169  suborng  33198  intlidl  33301  idlinsubrg  33312  rhmimaidl  33313  ssdifidllem  33337  ssmxidllem  33354  1arithidomlem1  33416  1arithidomlem2  33417  1arithidom  33418  minplyirred  33586  algextdeglem4  33593  algextdeglem8  33597  rtelextdg2lem  33599  2sqr3minply  33620  locfinreflem  33668  locfinref  33669  xrge0iifcnv  33761  xrge0iifiso  33763  xrge0iifhom  33765  esumc  33897  esumle  33904  esumlef  33908  esumpinfsum  33923  esumpcvgval  33924  fiunelros  34020  voliune  34075  volfiniune  34076  sibfinima  34186  eulerpartlemt  34218  fiblem  34245  fibp1  34248  dstrvprob  34318  ballotlemsel1i  34359  ballotlemfrceq  34375  plymulx0  34406  signstfvc  34433  signstfveq0  34436  bnj944  34796  bnj998  34815  bnj1136  34855  bnj1408  34894  erdszelem4  35035  erdszelem8  35039  txsconnlem  35081  cvxsconn  35084  cvmliftpht  35159  snmlff  35170  elmrsubrn  35361  msrf  35383  mthmpps  35423  sinccvglem  35513  trer  36041  poimirlem6  37340  poimirlem7  37341  poimirlem9  37343  poimirlem17  37351  poimirlem20  37354  poimirlem28  37362  poimirlem29  37363  poimirlem30  37364  poimirlem31  37365  poimirlem32  37366  areacirc  37427  nnubfi  37464  prter1  38590  lkrlss  38806  diaf11N  40761  dibf11N  40873  lclkr  41245  lclkrs  41251  lcfrlem9  41262  lcfr  41297  mapd1o  41360  hdmapf1oN  41577  hgmapf1oN  41615  sn-inelr  42178  frlmvscadiccat  42196  fimgmcyc  42224  nacsfix  42406  eldioph2lem1  42454  irrapxlem1  42516  rmxypairf1o  42606  jm2.27a  42700  hbtlem2  42822  hbt  42828  mon1psubm  42901  onnog  43133  pren2d  43260  binomcxplemnotnn0  44067  elixpconstg  44727  elfzfzo  44927  monoords  44948  elfzod  45051  eluzd  45060  fmul01lt1lem2  45242  sumnnodd  45287  ioodvbdlimc1lem2  45589  ioodvbdlimc2lem  45591  iblsplit  45623  iblspltprt  45630  itgspltprt  45636  stoweidlem11  45668  stoweidlem17  45674  fourierdlem12  45776  fourierdlem20  45784  fourierdlem25  45789  fourierdlem37  45801  fourierdlem41  45805  fourierdlem48  45811  fourierdlem49  45812  fourierdlem50  45813  fourierdlem54  45817  fourierdlem64  45827  fourierdlem73  45836  fourierdlem79  45842  fourierdlem102  45865  fourierdlem111  45874  fourierdlem114  45877  etransclem23  45914  etransclem48  45939  2elfz2melfz  46967  elfzlble  46969  iccpartiltu  47030  iccpartigtl  47031  iccpartlt  47032  iccpartgt  47035  lswn0  47052  fmtnoge3  47138  fmtnodvds  47152  odz2prm2pw  47171  fmtnole4prm  47186  lighneallem4b  47217  mogoldbb  47393  nnsum4primesevenALTV  47409  bgoldbtbndlem3  47415  ssnn0ssfz  47764  lmod1  47911  elfzolborelfzop1  47938  nnolog2flm1  48014