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 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  7283  limuni3  7804  onfununi  8283  smores2  8296  smoiso  8304  oelimcl  8538  iserd  8672  resixp  8883  undifixp  8884  alephval3  10032  canthwelem  10573  canthwe  10574  r1limwun  10659  wunex2  10661  tskcard  10704  gruina  10741  eluzmn  12770  eluzuzle  12772  uztrn  12781  eluzadd  12792  eluzsub  12793  subeluzsub  12796  nn0pzuz  12830  zsupss  12862  nn0ge2m1nnALT  12867  xov1plusxeqvd  13426  ige2m1fz  13545  0elfz  13552  uzsubfz0  13564  elfzmlbm  13566  difelfzle  13569  difelfznle  13570  fvffz0  13574  elfzolt2b  13598  elfzolt3b  13599  elfzouz2  13602  fzossrbm1  13616  elfzo0  13628  eluzgtdifelfzo  13655  elfzodifsumelfzo  13659  fzonn0p1  13670  fzonn0p1p1  13672  fzo0sn0fzo1  13683  ssfzo12bi  13689  fzoopth  13690  ubmelm1fzo  13691  elfzonelfzo  13697  fzosplitprm1  13706  fzostep1  13714  fvinim0ffz  13717  flword2  13745  uzsup  13795  modfzo0difsn  13878  modsumfzodifsn  13879  fsuppmapnn0fiub  13926  suppssfz  13929  1elfz0hash  14325  fzsdom2  14363  ccatdmss  14517  ccatrn  14525  ccat2s1fvw  14574  pfxn0  14622  pfxtrcfv0  14629  pfxtrcfvl  14632  swrdswrd  14640  swrdccatin1  14660  pfxccat3  14669  pfxccat3a  14673  repswswrd  14719  cshwidxmod  14738  cshw1  14757  cshwcsh2id  14763  swrds2  14875  pfx2  14882  2swrd2eqwrdeq  14888  ccat2s1fvwALT  14890  rexuzre  15288  limsupgre  15416  rlimclim1  15480  rlimclim  15481  climrlim2  15482  isercolllem1  15600  isercoll  15603  climcndslem1  15784  fallfacval4  15978  tanhbnd  16098  sinbnd2  16119  cosbnd2  16120  rpnnen2lem12  16162  nn0o  16322  bitsfzolem  16373  bitsfzo  16374  bitsmod  16375  bitsfi  16376  bitsinv1lem  16380  bitsinv1  16381  smueqlem  16429  dvdsnprmd  16629  2mulprm  16632  hashgcdlem  16727  prm23lt5  16754  zgz  16873  gznegcl  16875  gzcjcl  16876  gzaddcl  16877  gzmulcl  16878  vdwlem9  16929  prmgaplem3  16993  prmgaplem4  16994  cshwshashlem2  17036  setsstruct2  17113  ismred  17533  isfuncd  17801  homdmcoa  18003  isdrs2  18241  fpwipodrs  18475  ipodrsima  18476  chnub  18557  chnso  18559  sgrp2rid2ex  18864  subgid  19070  issubg2  19083  subsubg  19091  gaorber  19249  orbsta  19254  pmtrfconj  19407  psgnunilem2  19436  psgnunilem3  19437  psgnunilem4  19438  pgpfi1  19536  subgpgp  19538  pgpssslw  19555  subgslw  19557  sylow2alem2  19559  fislw  19566  sylow3lem3  19570  efgs1  19676  efgsp1  19678  efgsres  19679  efgredleme  19684  efgcpbllemb  19696  lt6abl  19836  telgsumfzs  19930  ablfac1eu  20016  submomnd  20073  isrngd  20120  prdsrngd  20123  ringrng  20232  isringrng  20234  isringd  20238  ringsrg  20244  ring1  20257  prdsringd  20268  subrngid  20494  subrngsubg  20497  issubrng2  20503  subsubrng  20508  subrgsubg  20522  subrgsubrng  20523  sdrgid  20737  cntzsdrg  20747  subdrgint  20748  sdrgint  20749  suborng  20821  islmodd  20829  islssd  20898  islss4  20925  dflidl2rng  21185  rnglidl0  21196  rnglidl1  21199  rnglidlrng  21214  rng2idlsubrng  21232  rhmpreimaidl  21244  gzrngunit  21400  expmhm  21403  zringunit  21433  prmirredlem  21439  znidomb  21528  isphld  21621  ocvocv  21638  ocvlss  21639  frlmlbs  21764  psdmul  22121  gsummoncoe1  22264  mp2pm2mplem4  22765  chfacfisf  22810  chfacfisfcpmat  22811  chfacfscmulfsupp  22815  chfacfpmmulfsupp  22819  chfacfpmmulgsum2  22821  2ndcctbss  23411  finlocfin  23476  dissnlocfin  23485  locfindis  23486  locfincf  23487  isfild  23814  infil  23819  neifil  23836  flimfcls  23982  istgp2  24047  oppgtmd  24053  oppgtgp  24054  distgp  24055  indistgp  24056  efmndtmd  24057  submtmd  24060  subgtgp  24061  symgtgp  24062  qustgplem  24077  prdstmdd  24080  prdstgpd  24081  tlmtgp  24152  isngp4  24568  subgngp  24591  ngptgp  24592  tngngp2  24608  nrgtrg  24646  nrgtdrg  24649  elii2  24900  icopnfcnv  24908  xrhmeo  24912  lebnumii  24933  phtpcer  24962  reparpht  24966  phtpcco2  24967  pcohtpy  24988  pcoass  24992  pcorevlem  24994  isclmi  25045  isncvsngpd  25118  cphsubrglem  25145  cphclm  25157  phclm  25200  tcphcph  25205  clsocv  25218  cphsscph  25219  cmslssbn  25340  pjthlem2  25406  ovolf  25451  iundisj2  25518  vitalilem2  25578  vitali  25582  itg2monolem3  25721  dvfsumlem1  26000  dvfsumlem3  26003  mon1puc1p  26124  uc1pmon1p  26125  mon1pid  26127  ply1remlem  26138  drnguc1p  26147  plyaddlem1  26186  coeidlem  26210  aannenlem2  26305  radcnvcl  26394  pilem2  26430  coseq00topi  26479  coseq0negpitopi  26480  tangtx  26482  tanabsge  26483  cosq14gt0  26487  cosq14ge0  26488  cosq34lt1  26504  cosordlem  26507  cos0pilt1  26509  sinord  26511  resinf1o  26513  tanord1  26514  tanord  26515  efif1olem3  26521  efsubm  26528  relogrn  26538  logimclad  26549  logrnaddcl  26551  logneg  26565  logcj  26583  argregt0  26587  argrege0  26588  argimgt0  26589  argimlt0  26590  logimul  26591  logneg2  26592  logdmnrp  26618  logcnlem4  26622  dvloglem  26625  logf1o2  26627  efopnlem2  26634  cxpsqrtlem  26679  relogbval  26750  nnlogbexp  26759  relogbcxp  26763  relogbcxpb  26765  logbgt0b  26771  asinneg  26864  asinsin  26870  acoscos  26871  acosbnd  26878  atancj  26888  atanlogaddlem  26891  atanlogsublem  26893  atanlogsub  26894  atantan  26901  atanbndlem  26903  atans2  26909  leibpi  26920  scvxcvx  26964  jensenlem2  26966  emcllem7  26980  basellem1  27059  ppisval  27082  chtdif  27136  ppidif  27141  ppiub  27183  chtublem  27190  chtub  27191  lgsdilem2  27312  gausslemma2dlem1a  27344  gausslemma2dlem2  27346  gausslemma2dlem5  27350  gausslemma2dlem6  27351  lgsquadlem1  27359  lgsquadlem2  27360  lgsquadlem3  27361  2lgslem1  27373  2sqlem3  27399  chebbnd1lem1  27448  chebbnd1lem2  27449  chebbnd1lem3  27450  dchrisumlem2  27469  dchrvmasumlem2  27477  dchrvmasumiflem1  27480  dchrisum0flblem2  27488  mulog2sumlem2  27514  logdivbnd  27535  pntpbnd2  27566  pntibndlem1  27568  pntibnd  27572  pntlemc  27574  pntlemg  27577  pntlemq  27580  pntlemf  27584  padicabvf  27610  padicabvcxp  27611  ostth2  27616  noextend  27646  noextendseq  27647  nosupno  27683  noinfno  27698  ttgcontlem1  28969  axpaschlem  29025  nbgr2vtx1edg  29435  nbuhgr2vtx1edgb  29437  cusgrexi  29528  structtocusgr  29531  pthdadjvtx  29813  pthdlem1  29851  pthd  29854  crctcshwlkn0lem3  29897  crctcshwlkn0lem4  29898  crctcshwlkn0lem5  29899  crctcshwlkn0lem7  29901  wlkiswwlks1  29952  wwlksm1edg  29966  wwlksnred  29977  wwlksnredwwlkn  29980  wwlksnextproplem3  29996  clwlkclwwlklem2fv1  30082  clwlkclwwlklem2fv2  30083  clwlkclwwlklem2a  30085  clwlkclwwlklem2  30087  clwwisshclwwslemlem  30100  clwwisshclwwslem  30101  erclwwlkref  30107  clwwlkel  30133  clwwlkf  30134  wwlksext2clwwlk  30144  wwlksubclwwlk  30145  umgr2cwwkdifex  30152  1pthd  30230  eucrctshift  30330  dlwwlknondlwlknonf1olem1  30451  numclwlk2lem2f  30464  frgrreggt1  30480  grpoinvf  30619  strlem3a  32339  hstrlem3a  32347  iundisj2f  32676  fcoinver  32690  fresf1o  32720  ssnnssfz  32877  bcm1n  32885  iundisj2fi  32887  fsumrp0cl  33113  cycpmco2lem6  33224  fxpsdrg  33268  lmodslmd  33297  fldgensdrg  33407  intlidl  33512  idlinsubrg  33523  rhmimaidl  33524  ssdifidllem  33548  ssmxidllem  33565  1arithidomlem1  33627  1arithidomlem2  33628  1arithidom  33629  fldextsdrg  33831  fldextrspunlem2  33854  fldextrspundgdvdslem  33857  fldextrspundgdvds  33858  minplyirred  33888  algextdeglem4  33897  algextdeglem8  33901  rtelextdg2lem  33903  constrsdrg  33952  2sqr3minply  33957  cos9thpiminply  33965  locfinreflem  34017  locfinref  34018  xrge0iifcnv  34110  xrge0iifiso  34112  xrge0iifhom  34114  esumc  34228  esumle  34235  esumlef  34239  esumpinfsum  34254  esumpcvgval  34255  fiunelros  34351  voliune  34406  volfiniune  34407  sibfinima  34516  eulerpartlemt  34548  fiblem  34575  fibp1  34578  dstrvprob  34649  ballotlemsel1i  34690  ballotlemfrceq  34706  plymulx0  34724  signstfvc  34751  signstfveq0  34754  bnj944  35113  bnj998  35132  bnj1136  35172  bnj1408  35211  erdszelem4  35407  erdszelem8  35411  txsconnlem  35453  cvxsconn  35456  cvmliftpht  35531  snmlff  35542  elmrsubrn  35733  msrf  35755  mthmpps  35795  sinccvglem  35885  trer  36529  poimirlem6  37874  poimirlem7  37875  poimirlem9  37877  poimirlem17  37885  poimirlem20  37888  poimirlem28  37896  poimirlem29  37897  poimirlem30  37898  poimirlem31  37899  poimirlem32  37900  areacirc  37961  nnubfi  37998  prter1  39252  lkrlss  39468  diaf11N  41422  dibf11N  41534  lclkr  41906  lclkrs  41912  lcfrlem9  41923  lcfr  41958  mapd1o  42021  hdmapf1oN  42238  hgmapf1oN  42276  frlmvscadiccat  42873  fimgmcyc  42901  nacsfix  43066  eldioph2lem1  43114  irrapxlem1  43176  rmxypairf1o  43265  jm2.27a  43359  hbtlem2  43478  hbt  43484  mon1psubm  43553  onnoxpg  43782  pren2d  43909  binomcxplemnotnn0  44709  elixpconstg  45445  elfzfzo  45636  monoords  45656  elfzod  45755  eluzd  45764  fmul01lt1lem2  45942  sumnnodd  45987  ioodvbdlimc1lem2  46287  ioodvbdlimc2lem  46289  iblsplit  46321  iblspltprt  46328  itgspltprt  46334  stoweidlem11  46366  stoweidlem17  46372  fourierdlem12  46474  fourierdlem20  46482  fourierdlem25  46487  fourierdlem37  46499  fourierdlem41  46503  fourierdlem48  46509  fourierdlem49  46510  fourierdlem50  46511  fourierdlem54  46515  fourierdlem64  46525  fourierdlem73  46534  fourierdlem79  46540  fourierdlem102  46563  fourierdlem111  46572  fourierdlem114  46575  etransclem23  46612  etransclem48  46637  ormkglobd  47230  chnsubseq  47235  2elfz2melfz  47675  elfzlble  47677  ceilhalfelfzo1  47687  1elfzo1ceilhalf1  47694  difltmodne  47699  modm2nep1  47723  modm1nep2  47725  modm1p1ne  47727  iccpartiltu  47779  iccpartigtl  47780  iccpartlt  47781  iccpartgt  47784  lswn0  47801  fmtnoge3  47887  fmtnodvds  47901  odz2prm2pw  47920  fmtnole4prm  47935  lighneallem4b  47966  mogoldbb  48142  nnsum4primesevenALTV  48158  bgoldbtbndlem3  48164  gpgprismgriedgdmss  48409  gpgprismgrusgra  48415  gpg3nbgrvtx0  48433  gpg3nbgrvtx0ALT  48434  gpg5nbgrvtx03star  48437  gpg5nbgr3star  48438  gpg3kgrtriexlem3  48442  gpg3kgrtriexlem4  48443  gpg3kgrtriexlem6  48445  gpgprismgr4cycllem3  48454  gpgprismgr4cycllem9  48460  ssnn0ssfz  48706  lmod1  48849  elfzolborelfzop1  48876  nnolog2flm1  48947  funcf2lem2  49438  isnatd  49579