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

Syntax hints:   → wi 4   ↔ wb 206   ∧ 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 207  df-an 396  df-3an 1088

This theorem is referenced by:  soisores  7273  limuni3  7794  onfununi  8273  smores2  8286  smoiso  8294  oelimcl  8528  iserd  8661  resixp  8871  undifixp  8872  alephval3  10020  canthwelem  10561  canthwe  10562  r1limwun  10647  wunex2  10649  tskcard  10692  gruina  10729  eluzmn  12758  eluzuzle  12760  uztrn  12769  eluzadd  12780  eluzsub  12781  subeluzsub  12784  nn0pzuz  12818  zsupss  12850  nn0ge2m1nnALT  12855  xov1plusxeqvd  13414  ige2m1fz  13533  0elfz  13540  uzsubfz0  13552  elfzmlbm  13554  difelfzle  13557  difelfznle  13558  fvffz0  13562  elfzolt2b  13586  elfzolt3b  13587  elfzouz2  13590  fzossrbm1  13604  elfzo0  13616  eluzgtdifelfzo  13643  elfzodifsumelfzo  13647  fzonn0p1  13658  fzonn0p1p1  13660  fzo0sn0fzo1  13671  ssfzo12bi  13677  fzoopth  13678  ubmelm1fzo  13679  elfzonelfzo  13685  fzosplitprm1  13694  fzostep1  13702  fvinim0ffz  13705  flword2  13733  uzsup  13783  modfzo0difsn  13866  modsumfzodifsn  13867  fsuppmapnn0fiub  13914  suppssfz  13917  1elfz0hash  14313  fzsdom2  14351  ccatdmss  14505  ccatrn  14513  ccat2s1fvw  14562  pfxn0  14610  pfxtrcfv0  14617  pfxtrcfvl  14620  swrdswrd  14628  swrdccatin1  14648  pfxccat3  14657  pfxccat3a  14661  repswswrd  14707  cshwidxmod  14726  cshw1  14745  cshwcsh2id  14751  swrds2  14863  pfx2  14870  2swrd2eqwrdeq  14876  ccat2s1fvwALT  14878  rexuzre  15276  limsupgre  15404  rlimclim1  15468  rlimclim  15469  climrlim2  15470  isercolllem1  15588  isercoll  15591  climcndslem1  15772  fallfacval4  15966  tanhbnd  16086  sinbnd2  16107  cosbnd2  16108  rpnnen2lem12  16150  nn0o  16310  bitsfzolem  16361  bitsfzo  16362  bitsmod  16363  bitsfi  16364  bitsinv1lem  16368  bitsinv1  16369  smueqlem  16417  dvdsnprmd  16617  2mulprm  16620  hashgcdlem  16715  prm23lt5  16742  zgz  16861  gznegcl  16863  gzcjcl  16864  gzaddcl  16865  gzmulcl  16866  vdwlem9  16917  prmgaplem3  16981  prmgaplem4  16982  cshwshashlem2  17024  setsstruct2  17101  ismred  17521  isfuncd  17789  homdmcoa  17991  isdrs2  18229  fpwipodrs  18463  ipodrsima  18464  chnub  18545  chnso  18547  sgrp2rid2ex  18852  subgid  19058  issubg2  19071  subsubg  19079  gaorber  19237  orbsta  19242  pmtrfconj  19395  psgnunilem2  19424  psgnunilem3  19425  psgnunilem4  19426  pgpfi1  19524  subgpgp  19526  pgpssslw  19543  subgslw  19545  sylow2alem2  19547  fislw  19554  sylow3lem3  19558  efgs1  19664  efgsp1  19666  efgsres  19667  efgredleme  19672  efgcpbllemb  19684  lt6abl  19824  telgsumfzs  19918  ablfac1eu  20004  submomnd  20061  isrngd  20108  prdsrngd  20111  ringrng  20220  isringrng  20222  isringd  20226  ringsrg  20232  ring1  20245  prdsringd  20256  subrngid  20482  subrngsubg  20485  issubrng2  20491  subsubrng  20496  subrgsubg  20510  subrgsubrng  20511  sdrgid  20725  cntzsdrg  20735  subdrgint  20736  sdrgint  20737  suborng  20809  islmodd  20817  islssd  20886  islss4  20913  dflidl2rng  21173  rnglidl0  21184  rnglidl1  21187  rnglidlrng  21202  rng2idlsubrng  21220  rhmpreimaidl  21232  gzrngunit  21388  expmhm  21391  zringunit  21421  prmirredlem  21427  znidomb  21516  isphld  21609  ocvocv  21626  ocvlss  21627  frlmlbs  21752  psdmul  22109  gsummoncoe1  22252  mp2pm2mplem4  22753  chfacfisf  22798  chfacfisfcpmat  22799  chfacfscmulfsupp  22803  chfacfpmmulfsupp  22807  chfacfpmmulgsum2  22809  2ndcctbss  23399  finlocfin  23464  dissnlocfin  23473  locfindis  23474  locfincf  23475  isfild  23802  infil  23807  neifil  23824  flimfcls  23970  istgp2  24035  oppgtmd  24041  oppgtgp  24042  distgp  24043  indistgp  24044  efmndtmd  24045  submtmd  24048  subgtgp  24049  symgtgp  24050  qustgplem  24065  prdstmdd  24068  prdstgpd  24069  tlmtgp  24140  isngp4  24556  subgngp  24579  ngptgp  24580  tngngp2  24596  nrgtrg  24634  nrgtdrg  24637  elii2  24888  icopnfcnv  24896  xrhmeo  24900  lebnumii  24921  phtpcer  24950  reparpht  24954  phtpcco2  24955  pcohtpy  24976  pcoass  24980  pcorevlem  24982  isclmi  25033  isncvsngpd  25106  cphsubrglem  25133  cphclm  25145  phclm  25188  tcphcph  25193  clsocv  25206  cphsscph  25207  cmslssbn  25328  pjthlem2  25394  ovolf  25439  iundisj2  25506  vitalilem2  25566  vitali  25570  itg2monolem3  25709  dvfsumlem1  25988  dvfsumlem3  25991  mon1puc1p  26112  uc1pmon1p  26113  mon1pid  26115  ply1remlem  26126  drnguc1p  26135  plyaddlem1  26174  coeidlem  26198  aannenlem2  26293  radcnvcl  26382  pilem2  26418  coseq00topi  26467  coseq0negpitopi  26468  tangtx  26470  tanabsge  26471  cosq14gt0  26475  cosq14ge0  26476  cosq34lt1  26492  cosordlem  26495  cos0pilt1  26497  sinord  26499  resinf1o  26501  tanord1  26502  tanord  26503  efif1olem3  26509  efsubm  26516  relogrn  26526  logimclad  26537  logrnaddcl  26539  logneg  26553  logcj  26571  argregt0  26575  argrege0  26576  argimgt0  26577  argimlt0  26578  logimul  26579  logneg2  26580  logdmnrp  26606  logcnlem4  26610  dvloglem  26613  logf1o2  26615  efopnlem2  26622  cxpsqrtlem  26667  relogbval  26738  nnlogbexp  26747  relogbcxp  26751  relogbcxpb  26753  logbgt0b  26759  asinneg  26852  asinsin  26858  acoscos  26859  acosbnd  26866  atancj  26876  atanlogaddlem  26879  atanlogsublem  26881  atanlogsub  26882  atantan  26889  atanbndlem  26891  atans2  26897  leibpi  26908  scvxcvx  26952  jensenlem2  26954  emcllem7  26968  basellem1  27047  ppisval  27070  chtdif  27124  ppidif  27129  ppiub  27171  chtublem  27178  chtub  27179  lgsdilem2  27300  gausslemma2dlem1a  27332  gausslemma2dlem2  27334  gausslemma2dlem5  27338  gausslemma2dlem6  27339  lgsquadlem1  27347  lgsquadlem2  27348  lgsquadlem3  27349  2lgslem1  27361  2sqlem3  27387  chebbnd1lem1  27436  chebbnd1lem2  27437  chebbnd1lem3  27438  dchrisumlem2  27457  dchrvmasumlem2  27465  dchrvmasumiflem1  27468  dchrisum0flblem2  27476  mulog2sumlem2  27502  logdivbnd  27523  pntpbnd2  27554  pntibndlem1  27556  pntibnd  27560  pntlemc  27562  pntlemg  27565  pntlemq  27568  pntlemf  27572  padicabvf  27598  padicabvcxp  27599  ostth2  27604  noextend  27634  noextendseq  27635  nosupno  27671  noinfno  27686  ttgcontlem1  28957  axpaschlem  29013  nbgr2vtx1edg  29423  nbuhgr2vtx1edgb  29425  cusgrexi  29516  structtocusgr  29519  pthdadjvtx  29801  pthdlem1  29839  pthd  29842  crctcshwlkn0lem3  29885  crctcshwlkn0lem4  29886  crctcshwlkn0lem5  29887  crctcshwlkn0lem7  29889  wlkiswwlks1  29940  wwlksm1edg  29954  wwlksnred  29965  wwlksnredwwlkn  29968  wwlksnextproplem3  29984  clwlkclwwlklem2fv1  30070  clwlkclwwlklem2fv2  30071  clwlkclwwlklem2a  30073  clwlkclwwlklem2  30075  clwwisshclwwslemlem  30088  clwwisshclwwslem  30089  erclwwlkref  30095  clwwlkel  30121  clwwlkf  30122  wwlksext2clwwlk  30132  wwlksubclwwlk  30133  umgr2cwwkdifex  30140  1pthd  30218  eucrctshift  30318  dlwwlknondlwlknonf1olem1  30439  numclwlk2lem2f  30452  frgrreggt1  30468  grpoinvf  30607  strlem3a  32327  hstrlem3a  32335  iundisj2f  32665  fcoinver  32679  fresf1o  32709  ssnnssfz  32867  bcm1n  32875  iundisj2fi  32877  fsumrp0cl  33103  cycpmco2lem6  33213  fxpsdrg  33257  lmodslmd  33286  fldgensdrg  33396  intlidl  33501  idlinsubrg  33512  rhmimaidl  33513  ssdifidllem  33537  ssmxidllem  33554  1arithidomlem1  33616  1arithidomlem2  33617  1arithidom  33618  fldextsdrg  33811  fldextrspunlem2  33834  fldextrspundgdvdslem  33837  fldextrspundgdvds  33838  minplyirred  33868  algextdeglem4  33877  algextdeglem8  33881  rtelextdg2lem  33883  constrsdrg  33932  2sqr3minply  33937  cos9thpiminply  33945  locfinreflem  33997  locfinref  33998  xrge0iifcnv  34090  xrge0iifiso  34092  xrge0iifhom  34094  esumc  34208  esumle  34215  esumlef  34219  esumpinfsum  34234  esumpcvgval  34235  fiunelros  34331  voliune  34386  volfiniune  34387  sibfinima  34496  eulerpartlemt  34528  fiblem  34555  fibp1  34558  dstrvprob  34629  ballotlemsel1i  34670  ballotlemfrceq  34686  plymulx0  34704  signstfvc  34731  signstfveq0  34734  bnj944  35094  bnj998  35113  bnj1136  35153  bnj1408  35192  erdszelem4  35388  erdszelem8  35392  txsconnlem  35434  cvxsconn  35437  cvmliftpht  35512  snmlff  35523  elmrsubrn  35714  msrf  35736  mthmpps  35776  sinccvglem  35866  trer  36510  poimirlem6  37823  poimirlem7  37824  poimirlem9  37826  poimirlem17  37834  poimirlem20  37837  poimirlem28  37845  poimirlem29  37846  poimirlem30  37847  poimirlem31  37848  poimirlem32  37849  areacirc  37910  nnubfi  37947  prter1  39135  lkrlss  39351  diaf11N  41305  dibf11N  41417  lclkr  41789  lclkrs  41795  lcfrlem9  41806  lcfr  41841  mapd1o  41904  hdmapf1oN  42121  hgmapf1oN  42159  frlmvscadiccat  42757  fimgmcyc  42785  nacsfix  42950  eldioph2lem1  42998  irrapxlem1  43060  rmxypairf1o  43149  jm2.27a  43243  hbtlem2  43362  hbt  43368  mon1psubm  43437  onnoxpg  43666  pren2d  43793  binomcxplemnotnn0  44593  elixpconstg  45329  elfzfzo  45521  monoords  45541  elfzod  45640  eluzd  45649  fmul01lt1lem2  45827  sumnnodd  45872  ioodvbdlimc1lem2  46172  ioodvbdlimc2lem  46174  iblsplit  46206  iblspltprt  46213  itgspltprt  46219  stoweidlem11  46251  stoweidlem17  46257  fourierdlem12  46359  fourierdlem20  46367  fourierdlem25  46372  fourierdlem37  46384  fourierdlem41  46388  fourierdlem48  46394  fourierdlem49  46395  fourierdlem50  46396  fourierdlem54  46400  fourierdlem64  46410  fourierdlem73  46419  fourierdlem79  46425  fourierdlem102  46448  fourierdlem111  46457  fourierdlem114  46460  etransclem23  46497  etransclem48  46522  ormkglobd  47115  chnsubseq  47120  2elfz2melfz  47560  elfzlble  47562  ceilhalfelfzo1  47572  1elfzo1ceilhalf1  47579  difltmodne  47584  modm2nep1  47608  modm1nep2  47610  modm1p1ne  47612  iccpartiltu  47664  iccpartigtl  47665  iccpartlt  47666  iccpartgt  47669  lswn0  47686  fmtnoge3  47772  fmtnodvds  47786  odz2prm2pw  47805  fmtnole4prm  47820  lighneallem4b  47851  mogoldbb  48027  nnsum4primesevenALTV  48043  bgoldbtbndlem3  48049  gpgprismgriedgdmss  48294  gpgprismgrusgra  48300  gpg3nbgrvtx0  48318  gpg3nbgrvtx0ALT  48319  gpg5nbgrvtx03star  48322  gpg5nbgr3star  48323  gpg3kgrtriexlem3  48327  gpg3kgrtriexlem4  48328  gpg3kgrtriexlem6  48330  gpgprismgr4cycllem3  48339  gpgprismgr4cycllem9  48345  ssnn0ssfz  48591  lmod1  48734  elfzolborelfzop1  48761  nnolog2flm1  48832  funcf2lem2  49323  isnatd  49464