Theorem syl3anbrc 1345

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ w3a 1089

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 210  df-an 400  df-3an 1091

This theorem is referenced by:  soisores  7125  limuni3  7620  onfununi  8067  smores2  8080  smoiso  8088  oelimcl  8317  iserd  8406  resixp  8603  undifixp  8604  alephval3  9707  canthwelem  10247  canthwe  10248  r1limwun  10333  wunex2  10335  tskcard  10378  gruina  10415  eluzmn  12428  eluzuzle  12430  uztrn  12439  subeluzsub  12454  nn0pzuz  12484  zsupss  12516  nn0ge2m1nnALT  12521  xov1plusxeqvd  13069  ige2m1fz  13185  0elfz  13192  uzsubfz0  13203  elfzmlbm  13205  difelfzle  13208  difelfznle  13209  fvffz0  13213  elfzolt2b  13237  elfzolt3b  13238  elfzouz2  13240  fzossrbm1  13254  elfzo0  13266  eluzgtdifelfzo  13287  elfzodifsumelfzo  13291  fzonn0p1  13302  fzonn0p1p1  13304  fzo0sn0fzo1  13314  ssfzo12bi  13320  ubmelm1fzo  13321  elfzonelfzo  13327  fzosplitprm1  13335  fzostep1  13341  fvinim0ffz  13344  flword2  13371  uzsup  13419  modfzo0difsn  13499  modsumfzodifsn  13500  fsuppmapnn0fiub  13547  suppssfz  13550  1elfz0hash  13940  fzsdom2  13978  ccatrn  14129  ccat2s1fvw  14184  ccat2s1fvwOLD  14185  pfxn0  14234  pfxtrcfv0  14242  pfxtrcfvl  14245  swrdswrd  14253  swrdccatin1  14273  pfxccat3  14282  pfxccat3a  14286  repswswrd  14332  cshwidxmod  14351  cshw1  14370  cshwcsh2id  14376  swrds2  14488  pfx2  14495  2swrd2eqwrdeq  14501  ccat2s1fvwALT  14504  ccat2s1fvwALTOLD  14505  rexuzre  14899  limsupgre  15025  rlimclim1  15089  rlimclim  15090  climrlim2  15091  isercolllem1  15211  isercoll  15214  climcndslem1  15394  fallfacval4  15586  tanhbnd  15703  sinbnd2  15724  cosbnd2  15725  rpnnen2lem12  15767  nn0o  15925  bitsfzolem  15974  bitsfzo  15975  bitsmod  15976  bitsfi  15977  bitsinv1lem  15981  bitsinv1  15982  smueqlem  16030  dvdsnprmd  16228  2mulprm  16231  hashgcdlem  16322  prm23lt5  16348  zgz  16467  gznegcl  16469  gzcjcl  16470  gzaddcl  16471  gzmulcl  16472  vdwlem9  16523  prmgaplem3  16587  prmgaplem4  16588  cshwshashlem2  16631  setsstruct2  16721  ismred  17077  isfuncd  17343  homdmcoa  17545  isdrs2  17785  fpwipodrs  18018  ipodrsima  18019  sgrp2rid2ex  18326  subgid  18517  issubg2  18530  subsubg  18538  gaorber  18674  orbsta  18679  pmtrfconj  18830  psgnunilem2  18859  psgnunilem3  18860  psgnunilem4  18861  pgpfi1  18956  subgpgp  18958  pgpssslw  18975  subgslw  18977  sylow2alem2  18979  fislw  18986  sylow3lem3  18990  efgs1  19097  efgsp1  19099  efgsres  19100  efgredleme  19105  efgcpbllemb  19117  lt6abl  19252  telgsumfzs  19346  ablfac1eu  19432  isringd  19575  ringsrg  19579  ring1  19592  prdsringd  19602  subrgsubg  19778  sdrgid  19812  cntzsdrg  19818  subdrgint  19819  sdrgint  19820  islmodd  19877  islssd  19944  islss4  19971  gzrngunit  20401  expmhm  20404  zringunit  20425  prmirredlem  20431  znidomb  20498  isphld  20588  ocvocv  20605  ocvlss  20606  frlmlbs  20731  gsummoncoe1  21197  mp2pm2mplem4  21678  chfacfisf  21723  chfacfisfcpmat  21724  chfacfscmulfsupp  21728  chfacfpmmulfsupp  21732  chfacfpmmulgsum2  21734  2ndcctbss  22324  finlocfin  22389  dissnlocfin  22398  locfindis  22399  locfincf  22400  isfild  22727  infil  22732  neifil  22749  flimfcls  22895  istgp2  22960  oppgtmd  22966  oppgtgp  22967  distgp  22968  indistgp  22969  efmndtmd  22970  submtmd  22973  subgtgp  22974  symgtgp  22975  qustgplem  22990  prdstmdd  22993  prdstgpd  22994  tlmtgp  23065  isngp4  23482  subgngp  23505  ngptgp  23506  tngngp2  23522  nrgtrg  23560  nrgtdrg  23563  elii2  23805  icopnfcnv  23811  xrhmeo  23815  lebnumii  23835  phtpcer  23864  reparpht  23867  phtpcco2  23868  pcohtpy  23889  pcoass  23893  pcorevlem  23895  isclmi  23946  isncvsngpd  24019  cphsubrglem  24046  cphclm  24058  phclm  24101  tcphcph  24106  clsocv  24119  cphsscph  24120  cmslssbn  24241  pjthlem2  24307  ovolf  24351  iundisj2  24418  vitalilem2  24478  vitali  24482  itg2monolem3  24622  dvfsumlem1  24895  dvfsumlem3  24897  mon1puc1p  25020  uc1pmon1p  25021  ply1remlem  25032  drnguc1p  25040  plyaddlem1  25079  coeidlem  25103  aannenlem2  25194  radcnvcl  25281  pilem2  25316  coseq00topi  25364  coseq0negpitopi  25365  tangtx  25367  tanabsge  25368  cosq14gt0  25372  cosq14ge0  25373  cosq34lt1  25388  cosordlem  25391  cos0pilt1  25393  sinord  25395  resinf1o  25397  tanord1  25398  tanord  25399  efif1olem3  25405  efsubm  25412  relogrn  25422  logimclad  25433  logrnaddcl  25435  logneg  25448  logcj  25466  argregt0  25470  argrege0  25471  argimgt0  25472  argimlt0  25473  logimul  25474  logneg2  25475  logdmnrp  25501  logcnlem4  25505  dvloglem  25508  logf1o2  25510  efopnlem2  25517  cxpsqrtlem  25562  relogbval  25627  nnlogbexp  25636  relogbcxp  25640  relogbcxpb  25642  logbgt0b  25648  asinneg  25741  asinsin  25747  acoscos  25748  acosbnd  25755  atancj  25765  atanlogaddlem  25768  atanlogsublem  25770  atanlogsub  25771  atantan  25778  atanbndlem  25780  atans2  25786  leibpi  25797  scvxcvx  25840  jensenlem2  25842  emcllem7  25856  basellem1  25935  ppisval  25958  chtdif  26012  ppidif  26017  ppiub  26057  chtublem  26064  chtub  26065  lgsdilem2  26186  gausslemma2dlem1a  26218  gausslemma2dlem2  26220  gausslemma2dlem5  26224  gausslemma2dlem6  26225  lgsquadlem1  26233  lgsquadlem2  26234  lgsquadlem3  26235  2lgslem1  26247  2sqlem3  26273  chebbnd1lem1  26322  chebbnd1lem2  26323  chebbnd1lem3  26324  dchrisumlem2  26343  dchrvmasumlem2  26351  dchrvmasumiflem1  26354  dchrisum0flblem2  26362  mulog2sumlem2  26388  logdivbnd  26409  pntpbnd2  26440  pntibndlem1  26442  pntibnd  26446  pntlemc  26448  pntlemg  26451  pntlemq  26454  pntlemf  26458  padicabvf  26484  padicabvcxp  26485  ostth2  26490  ttgcontlem1  26948  axpaschlem  27003  nbgr2vtx1edg  27410  nbuhgr2vtx1edgb  27412  cusgrexi  27503  structtocusgr  27506  pthdadjvtx  27789  pthdlem1  27825  pthd  27828  crctcshwlkn0lem3  27868  crctcshwlkn0lem4  27869  crctcshwlkn0lem5  27870  crctcshwlkn0lem7  27872  wlkiswwlks1  27923  wwlksm1edg  27937  wwlksnred  27948  wwlksnredwwlkn  27951  wwlksnextproplem3  27967  clwlkclwwlklem2fv1  28050  clwlkclwwlklem2fv2  28051  clwlkclwwlklem2a  28053  clwlkclwwlklem2  28055  clwwisshclwwslemlem  28068  clwwisshclwwslem  28069  erclwwlkref  28075  clwwlkel  28101  clwwlkf  28102  wwlksext2clwwlk  28112  wwlksubclwwlk  28113  umgr2cwwkdifex  28120  1pthd  28198  eucrctshift  28298  dlwwlknondlwlknonf1olem1  28419  numclwlk2lem2f  28432  frgrreggt1  28448  grpoinvf  28585  strlem3a  30305  hstrlem3a  30313  iundisj2f  30620  fcoinver  30637  fresf1o  30657  ssnnssfz  30800  bcm1n  30808  iundisj2fi  30810  fsumrp0cl  30995  submomnd  31027  cycpmco2lem6  31089  lmodslmd  31148  suborng  31205  intlidl  31288  rhmpreimaidl  31289  idlinsubrg  31294  rhmimaidl  31295  ssmxidllem  31327  locfinreflem  31476  locfinref  31477  xrge0iifcnv  31569  xrge0iifiso  31571  xrge0iifhom  31573  esumc  31703  esumle  31710  esumlef  31714  esumpinfsum  31729  esumpcvgval  31730  fiunelros  31826  voliune  31881  volfiniune  31882  sibfinima  31990  eulerpartlemt  32022  fiblem  32049  fibp1  32052  dstrvprob  32122  ballotlemsel1i  32163  ballotlemfrceq  32179  plymulx0  32210  signstfvc  32237  signstfveq0  32240  bnj944  32603  bnj998  32622  bnj1136  32662  bnj1408  32701  erdszelem4  32841  erdszelem8  32845  txsconnlem  32887  cvxsconn  32890  cvmliftpht  32965  snmlff  32976  elmrsubrn  33167  msrf  33189  mthmpps  33229  sinccvglem  33315  noextend  33563  noextendseq  33564  nosupno  33600  noinfno  33615  trer  34199  poimirlem6  35477  poimirlem7  35478  poimirlem9  35480  poimirlem17  35488  poimirlem20  35491  poimirlem28  35499  poimirlem29  35500  poimirlem30  35501  poimirlem31  35502  poimirlem32  35503  areacirc  35564  nnubfi  35602  prter1  36587  lkrlss  36803  diaf11N  38757  dibf11N  38869  lclkr  39241  lclkrs  39247  lcfrlem9  39258  lcfr  39293  mapd1o  39356  hdmapf1oN  39573  hgmapf1oN  39611  frlmvscadiccat  39902  sn-inelr  40095  nacsfix  40189  eldioph2lem1  40237  irrapxlem1  40299  rmxypairf1o  40388  jm2.27a  40482  hbtlem2  40604  hbt  40610  mon1pid  40685  mon1psubm  40686  pren2d  40791  binomcxplemnotnn0  41599  elixpconstg  42264  elfzfzo  42439  monoords  42461  elfzod  42565  eluzd  42574  fmul01lt1lem2  42755  sumnnodd  42800  ioodvbdlimc1lem2  43102  ioodvbdlimc2lem  43104  iblsplit  43136  iblspltprt  43143  itgspltprt  43149  stoweidlem11  43181  stoweidlem17  43187  fourierdlem12  43289  fourierdlem20  43297  fourierdlem25  43302  fourierdlem37  43314  fourierdlem41  43318  fourierdlem48  43324  fourierdlem49  43325  fourierdlem50  43326  fourierdlem54  43330  fourierdlem64  43340  fourierdlem73  43349  fourierdlem79  43355  fourierdlem102  43378  fourierdlem111  43387  fourierdlem114  43390  etransclem23  43427  etransclem48  43452  2elfz2melfz  44437  elfzlble  44439  fzoopth  44446  iccpartiltu  44501  iccpartigtl  44502  iccpartlt  44503  iccpartgt  44506  lswn0  44523  fmtnoge3  44609  fmtnodvds  44623  odz2prm2pw  44642  fmtnole4prm  44657  lighneallem4b  44688  mogoldbb  44864  nnsum4primesevenALTV  44880  bgoldbtbndlem3  44886  ringrng  45064  isringrng  45066  lidlrng  45112  ssnn0ssfz  45312  lmod1  45460  elfzolborelfzop1  45487  nnolog2flm1  45563