Theorem syl3anbrc 1342

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

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

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 397  df-3an 1088

This theorem is referenced by:  soisores  7207  limuni3  7708  onfununi  8181  smores2  8194  smoiso  8202  oelimcl  8440  iserd  8533  resixp  8730  undifixp  8731  alephval3  9875  canthwelem  10415  canthwe  10416  r1limwun  10501  wunex2  10503  tskcard  10546  gruina  10583  eluzmn  12598  eluzuzle  12600  uztrn  12609  subeluzsub  12624  nn0pzuz  12654  zsupss  12686  nn0ge2m1nnALT  12691  xov1plusxeqvd  13239  ige2m1fz  13355  0elfz  13362  uzsubfz0  13373  elfzmlbm  13375  difelfzle  13378  difelfznle  13379  fvffz0  13383  elfzolt2b  13407  elfzolt3b  13408  elfzouz2  13411  fzossrbm1  13425  elfzo0  13437  eluzgtdifelfzo  13458  elfzodifsumelfzo  13462  fzonn0p1  13473  fzonn0p1p1  13475  fzo0sn0fzo1  13485  ssfzo12bi  13491  ubmelm1fzo  13492  elfzonelfzo  13498  fzosplitprm1  13506  fzostep1  13512  fvinim0ffz  13515  flword2  13542  uzsup  13592  modfzo0difsn  13672  modsumfzodifsn  13673  fsuppmapnn0fiub  13720  suppssfz  13723  1elfz0hash  14114  fzsdom2  14152  ccatrn  14303  ccat2s1fvw  14358  ccat2s1fvwOLD  14359  pfxn0  14408  pfxtrcfv0  14416  pfxtrcfvl  14419  swrdswrd  14427  swrdccatin1  14447  pfxccat3  14456  pfxccat3a  14460  repswswrd  14506  cshwidxmod  14525  cshw1  14544  cshwcsh2id  14550  swrds2  14662  pfx2  14669  2swrd2eqwrdeq  14675  ccat2s1fvwALT  14678  ccat2s1fvwALTOLD  14679  rexuzre  15073  limsupgre  15199  rlimclim1  15263  rlimclim  15264  climrlim2  15265  isercolllem1  15385  isercoll  15388  climcndslem1  15570  fallfacval4  15762  tanhbnd  15879  sinbnd2  15900  cosbnd2  15901  rpnnen2lem12  15943  nn0o  16101  bitsfzolem  16150  bitsfzo  16151  bitsmod  16152  bitsfi  16153  bitsinv1lem  16157  bitsinv1  16158  smueqlem  16206  dvdsnprmd  16404  2mulprm  16407  hashgcdlem  16498  prm23lt5  16524  zgz  16643  gznegcl  16645  gzcjcl  16646  gzaddcl  16647  gzmulcl  16648  vdwlem9  16699  prmgaplem3  16763  prmgaplem4  16764  cshwshashlem2  16807  setsstruct2  16884  ismred  17320  isfuncd  17589  homdmcoa  17791  isdrs2  18033  fpwipodrs  18267  ipodrsima  18268  sgrp2rid2ex  18575  subgid  18766  issubg2  18779  subsubg  18787  gaorber  18923  orbsta  18928  pmtrfconj  19083  psgnunilem2  19112  psgnunilem3  19113  psgnunilem4  19114  pgpfi1  19209  subgpgp  19211  pgpssslw  19228  subgslw  19230  sylow2alem2  19232  fislw  19239  sylow3lem3  19243  efgs1  19350  efgsp1  19352  efgsres  19353  efgredleme  19358  efgcpbllemb  19370  lt6abl  19505  telgsumfzs  19599  ablfac1eu  19685  isringd  19833  ringsrg  19837  ring1  19850  prdsringd  19860  subrgsubg  20039  sdrgid  20073  cntzsdrg  20079  subdrgint  20080  sdrgint  20081  islmodd  20138  islssd  20206  islss4  20233  gzrngunit  20673  expmhm  20676  zringunit  20697  prmirredlem  20703  znidomb  20778  isphld  20868  ocvocv  20885  ocvlss  20886  frlmlbs  21013  gsummoncoe1  21484  mp2pm2mplem4  21967  chfacfisf  22012  chfacfisfcpmat  22013  chfacfscmulfsupp  22017  chfacfpmmulfsupp  22021  chfacfpmmulgsum2  22023  2ndcctbss  22615  finlocfin  22680  dissnlocfin  22689  locfindis  22690  locfincf  22691  isfild  23018  infil  23023  neifil  23040  flimfcls  23186  istgp2  23251  oppgtmd  23257  oppgtgp  23258  distgp  23259  indistgp  23260  efmndtmd  23261  submtmd  23264  subgtgp  23265  symgtgp  23266  qustgplem  23281  prdstmdd  23284  prdstgpd  23285  tlmtgp  23356  isngp4  23777  subgngp  23800  ngptgp  23801  tngngp2  23825  nrgtrg  23863  nrgtdrg  23866  elii2  24108  icopnfcnv  24114  xrhmeo  24118  lebnumii  24138  phtpcer  24167  reparpht  24170  phtpcco2  24171  pcohtpy  24192  pcoass  24196  pcorevlem  24198  isclmi  24249  isncvsngpd  24323  cphsubrglem  24350  cphclm  24362  phclm  24405  tcphcph  24410  clsocv  24423  cphsscph  24424  cmslssbn  24545  pjthlem2  24611  ovolf  24655  iundisj2  24722  vitalilem2  24782  vitali  24786  itg2monolem3  24926  dvfsumlem1  25199  dvfsumlem3  25201  mon1puc1p  25324  uc1pmon1p  25325  ply1remlem  25336  drnguc1p  25344  plyaddlem1  25383  coeidlem  25407  aannenlem2  25498  radcnvcl  25585  pilem2  25620  coseq00topi  25668  coseq0negpitopi  25669  tangtx  25671  tanabsge  25672  cosq14gt0  25676  cosq14ge0  25677  cosq34lt1  25692  cosordlem  25695  cos0pilt1  25697  sinord  25699  resinf1o  25701  tanord1  25702  tanord  25703  efif1olem3  25709  efsubm  25716  relogrn  25726  logimclad  25737  logrnaddcl  25739  logneg  25752  logcj  25770  argregt0  25774  argrege0  25775  argimgt0  25776  argimlt0  25777  logimul  25778  logneg2  25779  logdmnrp  25805  logcnlem4  25809  dvloglem  25812  logf1o2  25814  efopnlem2  25821  cxpsqrtlem  25866  relogbval  25931  nnlogbexp  25940  relogbcxp  25944  relogbcxpb  25946  logbgt0b  25952  asinneg  26045  asinsin  26051  acoscos  26052  acosbnd  26059  atancj  26069  atanlogaddlem  26072  atanlogsublem  26074  atanlogsub  26075  atantan  26082  atanbndlem  26084  atans2  26090  leibpi  26101  scvxcvx  26144  jensenlem2  26146  emcllem7  26160  basellem1  26239  ppisval  26262  chtdif  26316  ppidif  26321  ppiub  26361  chtublem  26368  chtub  26369  lgsdilem2  26490  gausslemma2dlem1a  26522  gausslemma2dlem2  26524  gausslemma2dlem5  26528  gausslemma2dlem6  26529  lgsquadlem1  26537  lgsquadlem2  26538  lgsquadlem3  26539  2lgslem1  26551  2sqlem3  26577  chebbnd1lem1  26626  chebbnd1lem2  26627  chebbnd1lem3  26628  dchrisumlem2  26647  dchrvmasumlem2  26655  dchrvmasumiflem1  26658  dchrisum0flblem2  26666  mulog2sumlem2  26692  logdivbnd  26713  pntpbnd2  26744  pntibndlem1  26746  pntibnd  26750  pntlemc  26752  pntlemg  26755  pntlemq  26758  pntlemf  26762  padicabvf  26788  padicabvcxp  26789  ostth2  26794  ttgcontlem1  27261  axpaschlem  27317  nbgr2vtx1edg  27726  nbuhgr2vtx1edgb  27728  cusgrexi  27819  structtocusgr  27822  pthdadjvtx  28107  pthdlem1  28143  pthd  28146  crctcshwlkn0lem3  28186  crctcshwlkn0lem4  28187  crctcshwlkn0lem5  28188  crctcshwlkn0lem7  28190  wlkiswwlks1  28241  wwlksm1edg  28255  wwlksnred  28266  wwlksnredwwlkn  28269  wwlksnextproplem3  28285  clwlkclwwlklem2fv1  28368  clwlkclwwlklem2fv2  28369  clwlkclwwlklem2a  28371  clwlkclwwlklem2  28373  clwwisshclwwslemlem  28386  clwwisshclwwslem  28387  erclwwlkref  28393  clwwlkel  28419  clwwlkf  28420  wwlksext2clwwlk  28430  wwlksubclwwlk  28431  umgr2cwwkdifex  28438  1pthd  28516  eucrctshift  28616  dlwwlknondlwlknonf1olem1  28737  numclwlk2lem2f  28750  frgrreggt1  28766  grpoinvf  28903  strlem3a  30623  hstrlem3a  30631  iundisj2f  30938  fcoinver  30955  fresf1o  30975  ssnnssfz  31117  bcm1n  31125  iundisj2fi  31127  fsumrp0cl  31313  submomnd  31345  cycpmco2lem6  31407  lmodslmd  31466  suborng  31523  intlidl  31611  rhmpreimaidl  31612  idlinsubrg  31617  rhmimaidl  31618  ssmxidllem  31650  locfinreflem  31799  locfinref  31800  xrge0iifcnv  31892  xrge0iifiso  31894  xrge0iifhom  31896  esumc  32028  esumle  32035  esumlef  32039  esumpinfsum  32054  esumpcvgval  32055  fiunelros  32151  voliune  32206  volfiniune  32207  sibfinima  32315  eulerpartlemt  32347  fiblem  32374  fibp1  32377  dstrvprob  32447  ballotlemsel1i  32488  ballotlemfrceq  32504  plymulx0  32535  signstfvc  32562  signstfveq0  32565  bnj944  32927  bnj998  32946  bnj1136  32986  bnj1408  33025  erdszelem4  33165  erdszelem8  33169  txsconnlem  33211  cvxsconn  33214  cvmliftpht  33289  snmlff  33300  elmrsubrn  33491  msrf  33513  mthmpps  33553  sinccvglem  33639  noextend  33878  noextendseq  33879  nosupno  33915  noinfno  33930  trer  34514  poimirlem6  35792  poimirlem7  35793  poimirlem9  35795  poimirlem17  35803  poimirlem20  35806  poimirlem28  35814  poimirlem29  35815  poimirlem30  35816  poimirlem31  35817  poimirlem32  35818  areacirc  35879  nnubfi  35917  prter1  36900  lkrlss  37116  diaf11N  39070  dibf11N  39182  lclkr  39554  lclkrs  39560  lcfrlem9  39571  lcfr  39606  mapd1o  39669  hdmapf1oN  39886  hgmapf1oN  39924  frlmvscadiccat  40244  sn-inelr  40442  nacsfix  40541  eldioph2lem1  40589  irrapxlem1  40651  rmxypairf1o  40740  jm2.27a  40834  hbtlem2  40956  hbt  40962  mon1pid  41037  mon1psubm  41038  pren2d  41170  binomcxplemnotnn0  41981  elixpconstg  42646  elfzfzo  42822  monoords  42843  elfzod  42947  eluzd  42956  fmul01lt1lem2  43133  sumnnodd  43178  ioodvbdlimc1lem2  43480  ioodvbdlimc2lem  43482  iblsplit  43514  iblspltprt  43521  itgspltprt  43527  stoweidlem11  43559  stoweidlem17  43565  fourierdlem12  43667  fourierdlem20  43675  fourierdlem25  43680  fourierdlem37  43692  fourierdlem41  43696  fourierdlem48  43702  fourierdlem49  43703  fourierdlem50  43704  fourierdlem54  43708  fourierdlem64  43718  fourierdlem73  43727  fourierdlem79  43733  fourierdlem102  43756  fourierdlem111  43765  fourierdlem114  43768  etransclem23  43805  etransclem48  43830  2elfz2melfz  44821  elfzlble  44823  fzoopth  44830  iccpartiltu  44885  iccpartigtl  44886  iccpartlt  44887  iccpartgt  44890  lswn0  44907  fmtnoge3  44993  fmtnodvds  45007  odz2prm2pw  45026  fmtnole4prm  45041  lighneallem4b  45072  mogoldbb  45248  nnsum4primesevenALTV  45264  bgoldbtbndlem3  45270  ringrng  45448  isringrng  45450  lidlrng  45496  ssnn0ssfz  45696  lmod1  45844  elfzolborelfzop1  45871  nnolog2flm1  45947