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 1129	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
5		syl3anbrc.4	. 2 ⊢ (𝜏 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))
6	4, 5	sylibr 233	1 ⊢ (𝜑 → 𝜏)

Syntax hints:   → wi 4   ↔ wb 205   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  soisores  7324  limuni3  7841  onfununi  8341  smores2  8354  smoiso  8362  oelimcl  8600  iserd  8729  resixp  8927  undifixp  8928  alephval3  10105  canthwelem  10645  canthwe  10646  r1limwun  10731  wunex2  10733  tskcard  10776  gruina  10813  eluzmn  12829  eluzuzle  12831  uztrn  12840  eluzadd  12851  eluzsub  12852  subeluzsub  12859  nn0pzuz  12889  zsupss  12921  nn0ge2m1nnALT  12926  xov1plusxeqvd  13475  ige2m1fz  13591  0elfz  13598  uzsubfz0  13609  elfzmlbm  13611  difelfzle  13614  difelfznle  13615  fvffz0  13619  elfzolt2b  13643  elfzolt3b  13644  elfzouz2  13647  fzossrbm1  13661  elfzo0  13673  eluzgtdifelfzo  13694  elfzodifsumelfzo  13698  fzonn0p1  13709  fzonn0p1p1  13711  fzo0sn0fzo1  13721  ssfzo12bi  13727  ubmelm1fzo  13728  elfzonelfzo  13734  fzosplitprm1  13742  fzostep1  13748  fvinim0ffz  13751  flword2  13778  uzsup  13828  modfzo0difsn  13908  modsumfzodifsn  13909  fsuppmapnn0fiub  13956  suppssfz  13959  1elfz0hash  14350  fzsdom2  14388  ccatrn  14539  ccat2s1fvw  14588  pfxn0  14636  pfxtrcfv0  14644  pfxtrcfvl  14647  swrdswrd  14655  swrdccatin1  14675  pfxccat3  14684  pfxccat3a  14688  repswswrd  14734  cshwidxmod  14753  cshw1  14772  cshwcsh2id  14779  swrds2  14891  pfx2  14898  2swrd2eqwrdeq  14904  ccat2s1fvwALT  14906  rexuzre  15299  limsupgre  15425  rlimclim1  15489  rlimclim  15490  climrlim2  15491  isercolllem1  15611  isercoll  15614  climcndslem1  15795  fallfacval4  15987  tanhbnd  16104  sinbnd2  16125  cosbnd2  16126  rpnnen2lem12  16168  nn0o  16326  bitsfzolem  16375  bitsfzo  16376  bitsmod  16377  bitsfi  16378  bitsinv1lem  16382  bitsinv1  16383  smueqlem  16431  dvdsnprmd  16627  2mulprm  16630  hashgcdlem  16721  prm23lt5  16747  zgz  16866  gznegcl  16868  gzcjcl  16869  gzaddcl  16870  gzmulcl  16871  vdwlem9  16922  prmgaplem3  16986  prmgaplem4  16987  cshwshashlem2  17030  setsstruct2  17107  ismred  17546  isfuncd  17815  homdmcoa  18017  isdrs2  18259  fpwipodrs  18493  ipodrsima  18494  sgrp2rid2ex  18808  subgid  19008  issubg2  19021  subsubg  19029  gaorber  19172  orbsta  19177  pmtrfconj  19334  psgnunilem2  19363  psgnunilem3  19364  psgnunilem4  19365  pgpfi1  19463  subgpgp  19465  pgpssslw  19482  subgslw  19484  sylow2alem2  19486  fislw  19493  sylow3lem3  19497  efgs1  19603  efgsp1  19605  efgsres  19606  efgredleme  19611  efgcpbllemb  19623  lt6abl  19763  telgsumfzs  19857  ablfac1eu  19943  isringd  20105  ringsrg  20109  ring1  20122  prdsringd  20134  subrgsubg  20325  sdrgid  20408  cntzsdrg  20418  subdrgint  20419  sdrgint  20420  islmodd  20477  islssd  20546  islss4  20573  dflidl2lem  20842  gzrngunit  21011  expmhm  21014  zringunit  21036  prmirredlem  21042  znidomb  21117  isphld  21207  ocvocv  21224  ocvlss  21225  frlmlbs  21352  gsummoncoe1  21828  mp2pm2mplem4  22311  chfacfisf  22356  chfacfisfcpmat  22357  chfacfscmulfsupp  22361  chfacfpmmulfsupp  22365  chfacfpmmulgsum2  22367  2ndcctbss  22959  finlocfin  23024  dissnlocfin  23033  locfindis  23034  locfincf  23035  isfild  23362  infil  23367  neifil  23384  flimfcls  23530  istgp2  23595  oppgtmd  23601  oppgtgp  23602  distgp  23603  indistgp  23604  efmndtmd  23605  submtmd  23608  subgtgp  23609  symgtgp  23610  qustgplem  23625  prdstmdd  23628  prdstgpd  23629  tlmtgp  23700  isngp4  24121  subgngp  24144  ngptgp  24145  tngngp2  24169  nrgtrg  24207  nrgtdrg  24210  elii2  24452  icopnfcnv  24458  xrhmeo  24462  lebnumii  24482  phtpcer  24511  reparpht  24514  phtpcco2  24515  pcohtpy  24536  pcoass  24540  pcorevlem  24542  isclmi  24593  isncvsngpd  24667  cphsubrglem  24694  cphclm  24706  phclm  24749  tcphcph  24754  clsocv  24767  cphsscph  24768  cmslssbn  24889  pjthlem2  24955  ovolf  24999  iundisj2  25066  vitalilem2  25126  vitali  25130  itg2monolem3  25270  dvfsumlem1  25543  dvfsumlem3  25545  mon1puc1p  25668  uc1pmon1p  25669  ply1remlem  25680  drnguc1p  25688  plyaddlem1  25727  coeidlem  25751  aannenlem2  25842  radcnvcl  25929  pilem2  25964  coseq00topi  26012  coseq0negpitopi  26013  tangtx  26015  tanabsge  26016  cosq14gt0  26020  cosq14ge0  26021  cosq34lt1  26036  cosordlem  26039  cos0pilt1  26041  sinord  26043  resinf1o  26045  tanord1  26046  tanord  26047  efif1olem3  26053  efsubm  26060  relogrn  26070  logimclad  26081  logrnaddcl  26083  logneg  26096  logcj  26114  argregt0  26118  argrege0  26119  argimgt0  26120  argimlt0  26121  logimul  26122  logneg2  26123  logdmnrp  26149  logcnlem4  26153  dvloglem  26156  logf1o2  26158  efopnlem2  26165  cxpsqrtlem  26210  relogbval  26277  nnlogbexp  26286  relogbcxp  26290  relogbcxpb  26292  logbgt0b  26298  asinneg  26391  asinsin  26397  acoscos  26398  acosbnd  26405  atancj  26415  atanlogaddlem  26418  atanlogsublem  26420  atanlogsub  26421  atantan  26428  atanbndlem  26430  atans2  26436  leibpi  26447  scvxcvx  26490  jensenlem2  26492  emcllem7  26506  basellem1  26585  ppisval  26608  chtdif  26662  ppidif  26667  ppiub  26707  chtublem  26714  chtub  26715  lgsdilem2  26836  gausslemma2dlem1a  26868  gausslemma2dlem2  26870  gausslemma2dlem5  26874  gausslemma2dlem6  26875  lgsquadlem1  26883  lgsquadlem2  26884  lgsquadlem3  26885  2lgslem1  26897  2sqlem3  26923  chebbnd1lem1  26972  chebbnd1lem2  26973  chebbnd1lem3  26974  dchrisumlem2  26993  dchrvmasumlem2  27001  dchrvmasumiflem1  27004  dchrisum0flblem2  27012  mulog2sumlem2  27038  logdivbnd  27059  pntpbnd2  27090  pntibndlem1  27092  pntibnd  27096  pntlemc  27098  pntlemg  27101  pntlemq  27104  pntlemf  27108  padicabvf  27134  padicabvcxp  27135  ostth2  27140  noextend  27169  noextendseq  27170  nosupno  27206  noinfno  27221  ttgcontlem1  28142  axpaschlem  28198  nbgr2vtx1edg  28607  nbuhgr2vtx1edgb  28609  cusgrexi  28700  structtocusgr  28703  pthdadjvtx  28987  pthdlem1  29023  pthd  29026  crctcshwlkn0lem3  29066  crctcshwlkn0lem4  29067  crctcshwlkn0lem5  29068  crctcshwlkn0lem7  29070  wlkiswwlks1  29121  wwlksm1edg  29135  wwlksnred  29146  wwlksnredwwlkn  29149  wwlksnextproplem3  29165  clwlkclwwlklem2fv1  29248  clwlkclwwlklem2fv2  29249  clwlkclwwlklem2a  29251  clwlkclwwlklem2  29253  clwwisshclwwslemlem  29266  clwwisshclwwslem  29267  erclwwlkref  29273  clwwlkel  29299  clwwlkf  29300  wwlksext2clwwlk  29310  wwlksubclwwlk  29311  umgr2cwwkdifex  29318  1pthd  29396  eucrctshift  29496  dlwwlknondlwlknonf1olem1  29617  numclwlk2lem2f  29630  frgrreggt1  29646  grpoinvf  29785  strlem3a  31505  hstrlem3a  31513  iundisj2f  31821  fcoinver  31835  fresf1o  31855  ssnnssfz  31998  bcm1n  32006  iundisj2fi  32008  fsumrp0cl  32196  submomnd  32228  cycpmco2lem6  32290  lmodslmd  32349  fldgensdrg  32404  suborng  32433  intlidl  32536  rhmpreimaidl  32537  idlinsubrg  32549  rhmimaidl  32550  ssmxidllem  32589  minplyirred  32770  algextdeglem1  32772  locfinreflem  32820  locfinref  32821  xrge0iifcnv  32913  xrge0iifiso  32915  xrge0iifhom  32917  esumc  33049  esumle  33056  esumlef  33060  esumpinfsum  33075  esumpcvgval  33076  fiunelros  33172  voliune  33227  volfiniune  33228  sibfinima  33338  eulerpartlemt  33370  fiblem  33397  fibp1  33400  dstrvprob  33470  ballotlemsel1i  33511  ballotlemfrceq  33527  plymulx0  33558  signstfvc  33585  signstfveq0  33588  bnj944  33949  bnj998  33968  bnj1136  34008  bnj1408  34047  erdszelem4  34185  erdszelem8  34189  txsconnlem  34231  cvxsconn  34234  cvmliftpht  34309  snmlff  34320  elmrsubrn  34511  msrf  34533  mthmpps  34573  sinccvglem  34657  trer  35201  poimirlem6  36494  poimirlem7  36495  poimirlem9  36497  poimirlem17  36505  poimirlem20  36508  poimirlem28  36516  poimirlem29  36517  poimirlem30  36518  poimirlem31  36519  poimirlem32  36520  areacirc  36581  nnubfi  36618  prter1  37749  lkrlss  37965  diaf11N  39920  dibf11N  40032  lclkr  40404  lclkrs  40410  lcfrlem9  40421  lcfr  40456  mapd1o  40519  hdmapf1oN  40736  hgmapf1oN  40774  frlmvscadiccat  41080  sn-inelr  41338  nacsfix  41450  eldioph2lem1  41498  irrapxlem1  41560  rmxypairf1o  41650  jm2.27a  41744  hbtlem2  41866  hbt  41872  mon1pid  41947  mon1psubm  41948  onnog  42180  pren2d  42307  binomcxplemnotnn0  43115  elixpconstg  43778  elfzfzo  43986  monoords  44007  elfzod  44110  eluzd  44119  fmul01lt1lem2  44301  sumnnodd  44346  ioodvbdlimc1lem2  44648  ioodvbdlimc2lem  44650  iblsplit  44682  iblspltprt  44689  itgspltprt  44695  stoweidlem11  44727  stoweidlem17  44733  fourierdlem12  44835  fourierdlem20  44843  fourierdlem25  44848  fourierdlem37  44860  fourierdlem41  44864  fourierdlem48  44870  fourierdlem49  44871  fourierdlem50  44872  fourierdlem54  44876  fourierdlem64  44886  fourierdlem73  44895  fourierdlem79  44901  fourierdlem102  44924  fourierdlem111  44933  fourierdlem114  44936  etransclem23  44973  etransclem48  44998  2elfz2melfz  46026  elfzlble  46028  fzoopth  46035  iccpartiltu  46090  iccpartigtl  46091  iccpartlt  46092  iccpartgt  46095  lswn0  46112  fmtnoge3  46198  fmtnodvds  46212  odz2prm2pw  46231  fmtnole4prm  46246  lighneallem4b  46277  mogoldbb  46453  nnsum4primesevenALTV  46469  bgoldbtbndlem3  46475  ringrng  46655  isringrng  46657  isrngd  46672  prdsrngd  46677  subrngid  46728  subrngsubg  46731  issubrng2  46737  subsubrng  46742  dflidl2rng  46750  rnglidl0  46752  rnglidl1  46753  rnglidlrng  46758  rng2idlsubrng  46760  ssnn0ssfz  47025  lmod1  47173  elfzolborelfzop1  47200  nnolog2flm1  47276