Theorem syl3anbrc 1362

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  soisores  7336  limuni3  7857  onfununi  8337  smores2  8350  smoiso  8358  oelimcl  8595  iserd  8730  resixp  8940  undifixp  8941  alephval3  10113  canthwelem  10653  canthwe  10654  r1limwun  10739  wunex2  10741  tskcard  10784  gruina  10821  eluzmn  12887  eluzuzle  12889  uztrn  12898  eluzadd  12909  eluzsub  12910  subeluzsub  12913  nn0pzuz  12947  zsupss  12979  nn0ge2m1nnALT  12984  xov1plusxeqvd  13543  ige2m1fz  13664  0elfz  13671  uzsubfz0  13683  elfzmlbm  13685  difelfzle  13688  difelfznle  13689  fvffz0  13693  elfzod  13710  elfzolt2b  13718  elfzolt3b  13719  elfzouz2  13722  fzossrbm1  13736  elfzo0  13748  eluzgtdifelfzo  13775  elfzodifsumelfzo  13779  fzonn0p1  13790  fzonn0p1p1  13792  fzo0sn0fzo1  13803  ssfzo12bi  13809  fzoopth  13810  ubmelm1fzo  13811  elfzonelfzo  13817  fzosplitprm1  13826  fzostep1  13834  fvinim0ffz  13837  flword2  13866  uzsup  13916  modfzo0difsn  13999  modsumfzodifsn  14000  fsuppmapnn0fiub  14047  suppssfz  14050  1elfz0hash  14446  fzsdom2  14485  ccatdmss  14639  ccatrn  14647  ccat2s1fvw  14698  pfxn0  14748  pfxtrcfv0  14755  pfxtrcfvl  14758  swrdswrd  14766  swrdccatin1  14786  pfxccat3  14795  pfxccat3a  14799  repswswrd  14847  cshwidxmod  14866  cshw1  14885  cshwcsh2id  14891  swrds2  15003  pfx2  15010  2swrd2eqwrdeq  15016  ccat2s1fvwALT  15018  rexuzre  15430  limsupgre  15558  rlimclim1  15622  rlimclim  15623  climrlim2  15624  isercolllem1  15742  isercoll  15745  climcndslem1  15929  fallfacval4  16122  tanhbnd  16242  sinbnd2  16263  cosbnd2  16264  rpnnen2lem12  16306  nn0o  16466  bitsfzolem  16517  bitsfzo  16518  bitsmod  16519  bitsfi  16520  bitsinv1lem  16524  bitsinv1  16525  smueqlem  16573  dvdsnprmd  16773  2mulprm  16776  hashgcdlem  16872  prm23lt5  16899  zgz  17018  gznegcl  17020  gzcjcl  17021  gzaddcl  17022  gzmulcl  17023  vdwlem9  17074  prmgaplem3  17138  prmgaplem4  17139  cshwshashlem2  17181  setsstruct2  17259  ismred  17679  isfuncd  17947  homdmcoa  18149  isdrs2  18387  fpwipodrs  18621  ipodrsima  18622  chnub  18703  chnso  18705  sgrp2rid2ex  19020  subgid  19225  issubg2  19239  subsubg  19247  gaorber  19409  orbsta  19414  pmtrfconj  19567  psgnunilem2  19596  psgnunilem3  19597  psgnunilem4  19598  pgpfi1  19696  subgpgp  19698  pgpssslw  19715  subgslw  19717  sylow2alem2  19719  fislw  19726  sylow3lem3  19730  efgs1  19836  efgsp1  19838  efgsres  19839  efgredleme  19844  efgcpbllemb  19856  lt6abl  19996  telgsumfzs  20090  ablfac1eu  20176  submomnd  20233  isrngd  20282  prdsrngd  20285  ringrng  20400  isringrng  20402  isringd  20407  ringsrg  20413  ring1  20426  prdsringd  20435  subrngid  20685  subrngsubg  20688  issubrng2  20694  subsubrng  20699  subrgsubg  20713  subrgsubrng  20714  sdrgid  20932  cntzsdrg  20942  subdrgint  20943  sdrgint  20944  suborng  21016  islmodd  21024  islssd  21093  islss4  21120  dflidl2rng  21380  rnglidl0  21392  rnglidl1  21395  unichnlidl  21399  rnglidlrng  21418  rng2idlsubrng  21441  rhmpreimaidl  21453  ssdifidllem  21521  gzrngunit  21620  expmhm  21623  zringunit  21653  prmirredlem  21659  znidomb  21748  isphld  21841  ocvocv  21858  ocvlss  21859  frlmlbs  21984  psdmul  22366  gsummoncoe1  22505  mp2pm2mplem4  23003  chfacfisf  23048  chfacfisfcpmat  23049  chfacfscmulfsupp  23053  chfacfpmmulfsupp  23057  chfacfpmmulgsum2  23059  2ndcctbss  23649  finlocfin  23714  dissnlocfin  23723  locfindis  23724  locfincf  23725  isfild  24052  infil  24057  neifil  24074  flimfcls  24220  istgp2  24285  oppgtmd  24291  oppgtgp  24292  distgp  24293  indistgp  24294  efmndtmd  24295  submtmd  24298  subgtgp  24299  symgtgp  24300  qustgplem  24315  prdstmdd  24318  prdstgpd  24319  tlmtgp  24390  isngp4  24806  subgngp  24829  ngptgp  24830  tngngp2  24846  nrgtrg  24884  nrgtdrg  24887  elii2  25132  icopnfcnv  25138  xrhmeo  25142  lebnumii  25162  phtpcer  25191  reparpht  25194  phtpcco2  25195  pcohtpy  25216  pcoass  25220  pcorevlem  25222  isclmi  25273  isncvsngpd  25346  cphsubrglem  25373  cphclm  25385  phclm  25428  tcphcph  25433  clsocv  25446  cphsscph  25447  cmslssbn  25568  pjthlem2  25634  ovolf  25678  iundisj2  25745  vitalilem2  25805  vitali  25809  itg2monolem3  25948  dvfsumlem1  26222  dvfsumlem3  26224  mon1puc1p  26345  uc1pmon1p  26346  mon1pid  26348  ply1remlem  26359  drnguc1p  26368  plyaddlem1  26407  coeidlem  26431  plyn0mulidp  26479  aannenlem2  26529  radcnvcl  26617  pilem2  26652  coseq00topi  26704  coseq0negpitopi  26705  tangtx  26707  tanabsge  26708  cosq14gt0  26712  cosq14ge0  26713  cosq34lt1  26729  cosordlem  26732  cos0pilt1  26734  sinord  26736  resinf1o  26738  tanord1  26739  tanord  26740  efif1olem3  26746  efsubm  26753  relogrn  26763  logimclad  26774  logrnaddcl  26776  logneg  26790  logcj  26808  argregt0  26812  argrege0  26813  argimgt0  26814  argimlt0  26815  logimul  26816  logneg2  26817  logdmnrp  26843  logcnlem4  26847  dvloglem  26850  logf1o2  26852  efopnlem2  26859  cxpsqrtlem  26904  relogbval  26974  nnlogbexp  26983  relogbcxp  26987  relogbcxpb  26989  logbgt0b  26995  asinneg  27088  asinsin  27094  acoscos  27095  acosbnd  27102  atancj  27112  atanlogaddlem  27115  atanlogsublem  27117  atanlogsub  27118  atantan  27125  atanbndlem  27127  atans2  27133  leibpi  27144  scvxcvx  27187  jensenlem2  27189  emcllem7  27203  basellem1  27282  ppisval  27305  chtdif  27359  ppidif  27364  ppiub  27405  chtublem  27412  chtub  27413  lgsdilem2  27534  gausslemma2dlem1a  27566  gausslemma2dlem2  27568  gausslemma2dlem5  27572  gausslemma2dlem6  27573  lgsquadlem1  27581  lgsquadlem2  27582  lgsquadlem3  27583  2lgslem1  27595  2sqlem3  27621  chebbnd1lem1  27670  chebbnd1lem2  27671  chebbnd1lem3  27672  dchrisumlem2  27691  dchrvmasumlem2  27699  dchrvmasumiflem1  27702  dchrisum0flblem2  27710  mulog2sumlem2  27736  logdivbnd  27757  pntpbnd2  27788  pntibndlem1  27790  pntibnd  27794  pntlemc  27796  pntlemg  27799  pntlemq  27802  pntlemf  27806  padicabvf  27832  padicabvcxp  27833  ostth2  27838  noextend  27867  noextendseq  27868  nosupno  27904  noinfno  27919  ttgcontlem1  29271  axpaschlem  29327  nbgr2vtx1edg  29737  nbuhgr2vtx1edgb  29739  cusgrexi  29830  structtocusgr  29833  pthdadjvtx  30114  pthdlem1  30152  pthd  30155  crctcshwlkn0lem3  30198  crctcshwlkn0lem4  30199  crctcshwlkn0lem5  30200  crctcshwlkn0lem7  30202  wlkiswwlks1  30253  wwlksm1edg  30267  wwlksnred  30278  wwlksnredwwlkn  30281  wwlksnextproplem3  30297  clwlkclwwlklem2fv1  30383  clwlkclwwlklem2fv2  30384  clwlkclwwlklem2a  30386  clwlkclwwlklem2  30388  clwwisshclwwslemlem  30401  clwwisshclwwslem  30402  erclwwlkref  30408  clwwlkel  30434  clwwlkf  30435  wwlksext2clwwlk  30445  wwlksubclwwlk  30446  umgr2cwwkdifex  30453  1pthd  30531  eucrctshift  30631  dlwwlknondlwlknonf1olem1  30752  numclwlk2lem2f  30765  frgrreggt1  30781  grpoinvf  30921  strlem3a  32641  hstrlem3a  32649  iundisj2f  32972  fcoinver  32986  fresf1o  33013  ssnnssfz  33169  bcm1n  33177  iundisj2fi  33179  fsumrp0cl  33372  cycpmco2lem6  33482  fxpsdrg  33526  lmodslmd  33555  fldgensdrg  33666  intlidl  33759  idlinsubrg  33770  rhmimaidl  33771  ssmxidllem  33787  dflringlem2  33816  1arithidomlem1  33856  1arithidomlem2  33857  1arithidom  33858  fldextsdrg  34075  fldextrspunlem2  34098  fldextrspundgdvdslem  34101  fldextrspundgdvds  34102  minplyirred  34132  algextdeglem4  34141  algextdeglem8  34145  rtelextdg2lem  34147  constrsdrg  34196  2sqr3minply  34201  cos9thpiminply  34209  locfinreflem  34261  locfinref  34262  xrge0iifcnv  34354  xrge0iifiso  34356  xrge0iifhom  34358  esumc  34472  esumle  34479  esumlef  34483  esumpinfsum  34498  esumpcvgval  34499  fiunelros  34596  voliune  34651  volfiniune  34652  sibfinima  34761  eulerpartlemt  34793  fiblem  34820  fibp1  34823  dstrvprob  34894  ballotlemsel1i  34935  ballotlemfrceq  34951  signstfvc  34993  signstfveq0  34996  bnj944  35358  bnj998  35377  bnj1136  35417  bnj1408  35456  erdszelem4  35707  erdszelem8  35711  txsconnlem  35753  cvxsconn  35756  cvmliftpht  35831  snmlff  35842  elmrsubrn  36033  msrf  36055  mthmpps  36095  sinccvglem  36185  trer  36868  poimirlem6  38318  poimirlem7  38319  poimirlem9  38321  poimirlem17  38329  poimirlem20  38332  poimirlem28  38340  poimirlem29  38341  poimirlem30  38342  poimirlem31  38343  poimirlem32  38344  areacirc  38405  nnubfi  38442  prter1  39694  lkrlss  39910  diaf11N  41864  dibf11N  41976  lclkr  42348  lclkrs  42354  lcfrlem9  42365  lcfr  42400  mapd1o  42463  hdmapf1oN  42680  hgmapf1oN  42718  frlmvscadiccat  43321  fimgmcyc  43343  nacsfix  43484  eldioph2lem1  43532  irrapxlem1  43590  rmxypairf1o  43679  jm2.27a  43773  hbtlem2  43892  hbt  43898  mon1psubm  43967  onnoxpg  44196  pren2d  44323  binomcxplemnotnn0  45107  elixpconstg  45848  elfzfzo  46037  monoords  46057  eluzd  46164  fmul01lt1lem2  46342  sumnnodd  46387  ioodvbdlimc1lem2  46687  ioodvbdlimc2lem  46689  iblsplit  46721  iblspltprt  46728  itgspltprt  46734  stoweidlem11  46766  stoweidlem17  46772  fourierdlem12  46874  fourierdlem20  46882  fourierdlem25  46887  fourierdlem37  46899  fourierdlem41  46903  fourierdlem48  46909  fourierdlem50  46911  fourierdlem54  46915  fourierdlem64  46925  fourierdlem73  46934  fourierdlem79  46940  fourierdlem102  46963  fourierdlem111  46972  fourierdlem114  46975  etransclem23  47012  etransclem48  47037  ormkglobd  47632  chnsubseq  47637  2elfz2melfz  48096  elfzlble  48098  ceilhalfelfzo1  48112  1elfzo1ceilhalf1  48119  difltmodne  48126  modm2nep1  48150  modm1nep2  48152  modm1p1ne  48154  iccpartiltu  48212  iccpartigtl  48213  iccpartlt  48214  iccpartgt  48217  lswn0  48234  fmtnoge3  48323  fmtnodvds  48337  odz2prm2pw  48356  fmtnole4prm  48371  lighneallem4b  48402  nprmdvdsfacm1lem3  48415  nprmdvdsfacm1lem4  48416  nprmdvdsfacm1  48417  mogoldbb  48591  nnsum4primesevenALTV  48607  bgoldbtbndlem3  48613  gpgprismgriedgdmss  48858  gpgprismgrusgra  48864  gpg3nbgrvtx0  48882  gpg3nbgrvtx0ALT  48883  gpg5nbgrvtx03star  48886  gpg5nbgr3star  48887  gpg3kgrtriexlem3  48891  gpg3kgrtriexlem4  48892  gpg3kgrtriexlem6  48894  gpgprismgr4cycllem3  48903  gpgprismgr4cycllem9  48909  ssnn0ssfz  49170  lmod1  49313  elfzolborelfzop1  49340  nnolog2flm1  49411  funcf2lem2  49901  isnatd  50042