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 234	1 ⊢ (𝜑 → 𝜏)

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

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 1089

This theorem is referenced by:  soisores  7347  limuni3  7873  onfununi  8381  smores2  8394  smoiso  8402  oelimcl  8638  iserd  8771  resixp  8973  undifixp  8974  alephval3  10150  canthwelem  10690  canthwe  10691  r1limwun  10776  wunex2  10778  tskcard  10821  gruina  10858  eluzmn  12885  eluzuzle  12887  uztrn  12896  eluzadd  12907  eluzsub  12908  subeluzsub  12915  nn0pzuz  12947  zsupss  12979  nn0ge2m1nnALT  12984  xov1plusxeqvd  13538  ige2m1fz  13657  0elfz  13664  uzsubfz0  13676  elfzmlbm  13678  difelfzle  13681  difelfznle  13682  fvffz0  13686  elfzolt2b  13710  elfzolt3b  13711  elfzouz2  13714  fzossrbm1  13728  elfzo0  13740  eluzgtdifelfzo  13766  elfzodifsumelfzo  13770  fzonn0p1  13781  fzonn0p1p1  13783  fzo0sn0fzo1  13794  ssfzo12bi  13800  fzoopth  13801  ubmelm1fzo  13802  elfzonelfzo  13808  fzosplitprm1  13816  fzostep1  13822  fvinim0ffz  13825  flword2  13853  uzsup  13903  modfzo0difsn  13984  modsumfzodifsn  13985  fsuppmapnn0fiub  14032  suppssfz  14035  1elfz0hash  14429  fzsdom2  14467  ccatrn  14627  ccat2s1fvw  14676  pfxn0  14724  pfxtrcfv0  14732  pfxtrcfvl  14735  swrdswrd  14743  swrdccatin1  14763  pfxccat3  14772  pfxccat3a  14776  repswswrd  14822  cshwidxmod  14841  cshw1  14860  cshwcsh2id  14867  swrds2  14979  pfx2  14986  2swrd2eqwrdeq  14992  ccat2s1fvwALT  14994  rexuzre  15391  limsupgre  15517  rlimclim1  15581  rlimclim  15582  climrlim2  15583  isercolllem1  15701  isercoll  15704  climcndslem1  15885  fallfacval4  16079  tanhbnd  16197  sinbnd2  16218  cosbnd2  16219  rpnnen2lem12  16261  nn0o  16420  bitsfzolem  16471  bitsfzo  16472  bitsmod  16473  bitsfi  16474  bitsinv1lem  16478  bitsinv1  16479  smueqlem  16527  dvdsnprmd  16727  2mulprm  16730  hashgcdlem  16825  prm23lt5  16852  zgz  16971  gznegcl  16973  gzcjcl  16974  gzaddcl  16975  gzmulcl  16976  vdwlem9  17027  prmgaplem3  17091  prmgaplem4  17092  cshwshashlem2  17134  setsstruct2  17211  ismred  17645  isfuncd  17910  homdmcoa  18112  isdrs2  18352  fpwipodrs  18585  ipodrsima  18586  sgrp2rid2ex  18940  subgid  19146  issubg2  19159  subsubg  19167  gaorber  19326  orbsta  19331  pmtrfconj  19484  psgnunilem2  19513  psgnunilem3  19514  psgnunilem4  19515  pgpfi1  19613  subgpgp  19615  pgpssslw  19632  subgslw  19634  sylow2alem2  19636  fislw  19643  sylow3lem3  19647  efgs1  19753  efgsp1  19755  efgsres  19756  efgredleme  19761  efgcpbllemb  19773  lt6abl  19913  telgsumfzs  20007  ablfac1eu  20093  isrngd  20170  prdsrngd  20173  ringrng  20282  isringrng  20284  isringd  20288  ringsrg  20294  ring1  20307  prdsringd  20318  subrngid  20549  subrngsubg  20552  issubrng2  20558  subsubrng  20563  subrgsubg  20577  subrgsubrng  20578  sdrgid  20793  cntzsdrg  20803  subdrgint  20804  sdrgint  20805  islmodd  20864  islssd  20933  islss4  20960  dflidl2rng  21228  rnglidl0  21239  rnglidl1  21242  rnglidlrng  21257  rng2idlsubrng  21275  rhmpreimaidl  21287  gzrngunit  21451  expmhm  21454  zringunit  21477  prmirredlem  21483  znidomb  21580  isphld  21672  ocvocv  21689  ocvlss  21690  frlmlbs  21817  psdmul  22170  gsummoncoe1  22312  mp2pm2mplem4  22815  chfacfisf  22860  chfacfisfcpmat  22861  chfacfscmulfsupp  22865  chfacfpmmulfsupp  22869  chfacfpmmulgsum2  22871  2ndcctbss  23463  finlocfin  23528  dissnlocfin  23537  locfindis  23538  locfincf  23539  isfild  23866  infil  23871  neifil  23888  flimfcls  24034  istgp2  24099  oppgtmd  24105  oppgtgp  24106  distgp  24107  indistgp  24108  efmndtmd  24109  submtmd  24112  subgtgp  24113  symgtgp  24114  qustgplem  24129  prdstmdd  24132  prdstgpd  24133  tlmtgp  24204  isngp4  24625  subgngp  24648  ngptgp  24649  tngngp2  24673  nrgtrg  24711  nrgtdrg  24714  elii2  24965  icopnfcnv  24973  xrhmeo  24977  lebnumii  24998  phtpcer  25027  reparpht  25031  phtpcco2  25032  pcohtpy  25053  pcoass  25057  pcorevlem  25059  isclmi  25110  isncvsngpd  25184  cphsubrglem  25211  cphclm  25223  phclm  25266  tcphcph  25271  clsocv  25284  cphsscph  25285  cmslssbn  25406  pjthlem2  25472  ovolf  25517  iundisj2  25584  vitalilem2  25644  vitali  25648  itg2monolem3  25787  dvfsumlem1  26066  dvfsumlem3  26069  mon1puc1p  26190  uc1pmon1p  26191  mon1pid  26193  ply1remlem  26204  drnguc1p  26213  plyaddlem1  26252  coeidlem  26276  aannenlem2  26371  radcnvcl  26460  pilem2  26496  coseq00topi  26544  coseq0negpitopi  26545  tangtx  26547  tanabsge  26548  cosq14gt0  26552  cosq14ge0  26553  cosq34lt1  26569  cosordlem  26572  cos0pilt1  26574  sinord  26576  resinf1o  26578  tanord1  26579  tanord  26580  efif1olem3  26586  efsubm  26593  relogrn  26603  logimclad  26614  logrnaddcl  26616  logneg  26630  logcj  26648  argregt0  26652  argrege0  26653  argimgt0  26654  argimlt0  26655  logimul  26656  logneg2  26657  logdmnrp  26683  logcnlem4  26687  dvloglem  26690  logf1o2  26692  efopnlem2  26699  cxpsqrtlem  26744  relogbval  26815  nnlogbexp  26824  relogbcxp  26828  relogbcxpb  26830  logbgt0b  26836  asinneg  26929  asinsin  26935  acoscos  26936  acosbnd  26943  atancj  26953  atanlogaddlem  26956  atanlogsublem  26958  atanlogsub  26959  atantan  26966  atanbndlem  26968  atans2  26974  leibpi  26985  scvxcvx  27029  jensenlem2  27031  emcllem7  27045  basellem1  27124  ppisval  27147  chtdif  27201  ppidif  27206  ppiub  27248  chtublem  27255  chtub  27256  lgsdilem2  27377  gausslemma2dlem1a  27409  gausslemma2dlem2  27411  gausslemma2dlem5  27415  gausslemma2dlem6  27416  lgsquadlem1  27424  lgsquadlem2  27425  lgsquadlem3  27426  2lgslem1  27438  2sqlem3  27464  chebbnd1lem1  27513  chebbnd1lem2  27514  chebbnd1lem3  27515  dchrisumlem2  27534  dchrvmasumlem2  27542  dchrvmasumiflem1  27545  dchrisum0flblem2  27553  mulog2sumlem2  27579  logdivbnd  27600  pntpbnd2  27631  pntibndlem1  27633  pntibnd  27637  pntlemc  27639  pntlemg  27642  pntlemq  27645  pntlemf  27649  padicabvf  27675  padicabvcxp  27676  ostth2  27681  noextend  27711  noextendseq  27712  nosupno  27748  noinfno  27763  ttgcontlem1  28899  axpaschlem  28955  nbgr2vtx1edg  29367  nbuhgr2vtx1edgb  29369  cusgrexi  29460  structtocusgr  29463  pthdadjvtx  29748  pthdlem1  29786  pthd  29789  crctcshwlkn0lem3  29832  crctcshwlkn0lem4  29833  crctcshwlkn0lem5  29834  crctcshwlkn0lem7  29836  wlkiswwlks1  29887  wwlksm1edg  29901  wwlksnred  29912  wwlksnredwwlkn  29915  wwlksnextproplem3  29931  clwlkclwwlklem2fv1  30014  clwlkclwwlklem2fv2  30015  clwlkclwwlklem2a  30017  clwlkclwwlklem2  30019  clwwisshclwwslemlem  30032  clwwisshclwwslem  30033  erclwwlkref  30039  clwwlkel  30065  clwwlkf  30066  wwlksext2clwwlk  30076  wwlksubclwwlk  30077  umgr2cwwkdifex  30084  1pthd  30162  eucrctshift  30262  dlwwlknondlwlknonf1olem1  30383  numclwlk2lem2f  30396  frgrreggt1  30412  grpoinvf  30551  strlem3a  32271  hstrlem3a  32279  iundisj2f  32603  fcoinver  32617  fresf1o  32641  ssnnssfz  32789  bcm1n  32797  iundisj2fi  32799  ccatdmss  32934  chnub  33002  chnso  33004  fsumrp0cl  33026  submomnd  33087  cycpmco2lem6  33151  lmodslmd  33210  fldgensdrg  33316  suborng  33345  intlidl  33448  idlinsubrg  33459  rhmimaidl  33460  ssdifidllem  33484  ssmxidllem  33501  1arithidomlem1  33563  1arithidomlem2  33564  1arithidom  33565  fldextrspunlem2  33727  fldextrspundgdvdslem  33730  fldextrspundgdvds  33731  minplyirred  33754  algextdeglem4  33761  algextdeglem8  33765  rtelextdg2lem  33767  2sqr3minply  33791  locfinreflem  33839  locfinref  33840  xrge0iifcnv  33932  xrge0iifiso  33934  xrge0iifhom  33936  esumc  34052  esumle  34059  esumlef  34063  esumpinfsum  34078  esumpcvgval  34079  fiunelros  34175  voliune  34230  volfiniune  34231  sibfinima  34341  eulerpartlemt  34373  fiblem  34400  fibp1  34403  dstrvprob  34474  ballotlemsel1i  34515  ballotlemfrceq  34531  plymulx0  34562  signstfvc  34589  signstfveq0  34592  bnj944  34952  bnj998  34971  bnj1136  35011  bnj1408  35050  erdszelem4  35199  erdszelem8  35203  txsconnlem  35245  cvxsconn  35248  cvmliftpht  35323  snmlff  35334  elmrsubrn  35525  msrf  35547  mthmpps  35587  sinccvglem  35677  trer  36317  poimirlem6  37633  poimirlem7  37634  poimirlem9  37636  poimirlem17  37644  poimirlem20  37647  poimirlem28  37655  poimirlem29  37656  poimirlem30  37657  poimirlem31  37658  poimirlem32  37659  areacirc  37720  nnubfi  37757  prter1  38880  lkrlss  39096  diaf11N  41051  dibf11N  41163  lclkr  41535  lclkrs  41541  lcfrlem9  41552  lcfr  41587  mapd1o  41650  hdmapf1oN  41867  hgmapf1oN  41905  sn-inelr  42497  frlmvscadiccat  42516  fimgmcyc  42544  nacsfix  42723  eldioph2lem1  42771  irrapxlem1  42833  rmxypairf1o  42923  jm2.27a  43017  hbtlem2  43136  hbt  43142  mon1psubm  43211  onnog  43442  pren2d  43569  binomcxplemnotnn0  44375  elixpconstg  45094  elfzfzo  45288  monoords  45309  elfzod  45411  eluzd  45420  fmul01lt1lem2  45600  sumnnodd  45645  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  iblsplit  45981  iblspltprt  45988  itgspltprt  45994  stoweidlem11  46026  stoweidlem17  46032  fourierdlem12  46134  fourierdlem20  46142  fourierdlem25  46147  fourierdlem37  46159  fourierdlem41  46163  fourierdlem48  46169  fourierdlem49  46170  fourierdlem50  46171  fourierdlem54  46175  fourierdlem64  46185  fourierdlem73  46194  fourierdlem79  46200  fourierdlem102  46223  fourierdlem111  46232  fourierdlem114  46235  etransclem23  46272  etransclem48  46297  ormkglobd  46890  2elfz2melfz  47330  elfzlble  47332  difltmodne  47344  iccpartiltu  47409  iccpartigtl  47410  iccpartlt  47411  iccpartgt  47414  lswn0  47431  fmtnoge3  47517  fmtnodvds  47531  odz2prm2pw  47550  fmtnole4prm  47565  lighneallem4b  47596  mogoldbb  47772  nnsum4primesevenALTV  47788  bgoldbtbndlem3  47794  grlimgrtrilem1  47961  ceilhalfelfzo1  48016  gpg3nbgrvtx0  48032  gpg3nbgrvtx0ALT  48033  gpg5nbgrvtx03star  48036  gpg5nbgr3star  48037  gpg3kgrtriexlem3  48041  gpg3kgrtriexlem4  48042  gpg3kgrtriexlem6  48044  ssnn0ssfz  48265  lmod1  48409  elfzolborelfzop1  48436  nnolog2flm1  48511  funcf2lem2  48915  isnatd  48949