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  7282  limuni3  7803  onfununi  8281  smores2  8294  smoiso  8302  oelimcl  8536  iserd  8670  resixp  8881  undifixp  8882  alephval3  10032  canthwelem  10573  canthwe  10574  r1limwun  10659  wunex2  10661  tskcard  10704  gruina  10741  eluzmn  12795  eluzuzle  12797  uztrn  12806  eluzadd  12817  eluzsub  12818  subeluzsub  12821  nn0pzuz  12855  zsupss  12887  nn0ge2m1nnALT  12892  xov1plusxeqvd  13451  ige2m1fz  13571  0elfz  13578  uzsubfz0  13590  elfzmlbm  13592  difelfzle  13595  difelfznle  13596  fvffz0  13600  elfzod  13617  elfzolt2b  13625  elfzolt3b  13626  elfzouz2  13629  fzossrbm1  13643  elfzo0  13655  eluzgtdifelfzo  13682  elfzodifsumelfzo  13686  fzonn0p1  13697  fzonn0p1p1  13699  fzo0sn0fzo1  13710  ssfzo12bi  13716  fzoopth  13717  ubmelm1fzo  13718  elfzonelfzo  13724  fzosplitprm1  13733  fzostep1  13741  fvinim0ffz  13744  flword2  13772  uzsup  13822  modfzo0difsn  13905  modsumfzodifsn  13906  fsuppmapnn0fiub  13953  suppssfz  13956  1elfz0hash  14352  fzsdom2  14390  ccatdmss  14544  ccatrn  14552  ccat2s1fvw  14601  pfxn0  14649  pfxtrcfv0  14656  pfxtrcfvl  14659  swrdswrd  14667  swrdccatin1  14687  pfxccat3  14696  pfxccat3a  14700  repswswrd  14746  cshwidxmod  14765  cshw1  14784  cshwcsh2id  14790  swrds2  14902  pfx2  14909  2swrd2eqwrdeq  14915  ccat2s1fvwALT  14917  rexuzre  15315  limsupgre  15443  rlimclim1  15507  rlimclim  15508  climrlim2  15509  isercolllem1  15627  isercoll  15630  climcndslem1  15814  fallfacval4  16008  tanhbnd  16128  sinbnd2  16149  cosbnd2  16150  rpnnen2lem12  16192  nn0o  16352  bitsfzolem  16403  bitsfzo  16404  bitsmod  16405  bitsfi  16406  bitsinv1lem  16410  bitsinv1  16411  smueqlem  16459  dvdsnprmd  16659  2mulprm  16662  hashgcdlem  16758  prm23lt5  16785  zgz  16904  gznegcl  16906  gzcjcl  16907  gzaddcl  16908  gzmulcl  16909  vdwlem9  16960  prmgaplem3  17024  prmgaplem4  17025  cshwshashlem2  17067  setsstruct2  17144  ismred  17564  isfuncd  17832  homdmcoa  18034  isdrs2  18272  fpwipodrs  18506  ipodrsima  18507  chnub  18588  chnso  18590  sgrp2rid2ex  18898  subgid  19104  issubg2  19117  subsubg  19125  gaorber  19283  orbsta  19288  pmtrfconj  19441  psgnunilem2  19470  psgnunilem3  19471  psgnunilem4  19472  pgpfi1  19570  subgpgp  19572  pgpssslw  19589  subgslw  19591  sylow2alem2  19593  fislw  19600  sylow3lem3  19604  efgs1  19710  efgsp1  19712  efgsres  19713  efgredleme  19718  efgcpbllemb  19730  lt6abl  19870  telgsumfzs  19964  ablfac1eu  20050  submomnd  20107  isrngd  20154  prdsrngd  20157  ringrng  20266  isringrng  20268  isringd  20272  ringsrg  20278  ring1  20291  prdsringd  20300  subrngid  20526  subrngsubg  20529  issubrng2  20535  subsubrng  20540  subrgsubg  20554  subrgsubrng  20555  sdrgid  20769  cntzsdrg  20779  subdrgint  20780  sdrgint  20781  suborng  20853  islmodd  20861  islssd  20930  islss4  20957  dflidl2rng  21216  rnglidl0  21227  rnglidl1  21230  rnglidlrng  21245  rng2idlsubrng  21263  rhmpreimaidl  21275  gzrngunit  21413  expmhm  21416  zringunit  21446  prmirredlem  21452  znidomb  21541  isphld  21634  ocvocv  21651  ocvlss  21652  frlmlbs  21777  psdmul  22132  gsummoncoe1  22273  mp2pm2mplem4  22774  chfacfisf  22819  chfacfisfcpmat  22820  chfacfscmulfsupp  22824  chfacfpmmulfsupp  22828  chfacfpmmulgsum2  22830  2ndcctbss  23420  finlocfin  23485  dissnlocfin  23494  locfindis  23495  locfincf  23496  isfild  23823  infil  23828  neifil  23845  flimfcls  23991  istgp2  24056  oppgtmd  24062  oppgtgp  24063  distgp  24064  indistgp  24065  efmndtmd  24066  submtmd  24069  subgtgp  24070  symgtgp  24071  qustgplem  24086  prdstmdd  24089  prdstgpd  24090  tlmtgp  24161  isngp4  24577  subgngp  24600  ngptgp  24601  tngngp2  24617  nrgtrg  24655  nrgtdrg  24658  elii2  24903  icopnfcnv  24909  xrhmeo  24913  lebnumii  24933  phtpcer  24962  reparpht  24965  phtpcco2  24966  pcohtpy  24987  pcoass  24991  pcorevlem  24993  isclmi  25044  isncvsngpd  25117  cphsubrglem  25144  cphclm  25156  phclm  25199  tcphcph  25204  clsocv  25217  cphsscph  25218  cmslssbn  25339  pjthlem2  25405  ovolf  25449  iundisj2  25516  vitalilem2  25576  vitali  25580  itg2monolem3  25719  dvfsumlem1  25993  dvfsumlem3  25995  mon1puc1p  26116  uc1pmon1p  26117  mon1pid  26119  ply1remlem  26130  drnguc1p  26139  plyaddlem1  26178  coeidlem  26202  aannenlem2  26295  radcnvcl  26382  pilem2  26417  coseq00topi  26466  coseq0negpitopi  26467  tangtx  26469  tanabsge  26470  cosq14gt0  26474  cosq14ge0  26475  cosq34lt1  26491  cosordlem  26494  cos0pilt1  26496  sinord  26498  resinf1o  26500  tanord1  26501  tanord  26502  efif1olem3  26508  efsubm  26515  relogrn  26525  logimclad  26536  logrnaddcl  26538  logneg  26552  logcj  26570  argregt0  26574  argrege0  26575  argimgt0  26576  argimlt0  26577  logimul  26578  logneg2  26579  logdmnrp  26605  logcnlem4  26609  dvloglem  26612  logf1o2  26614  efopnlem2  26621  cxpsqrtlem  26666  relogbval  26736  nnlogbexp  26745  relogbcxp  26749  relogbcxpb  26751  logbgt0b  26757  asinneg  26850  asinsin  26856  acoscos  26857  acosbnd  26864  atancj  26874  atanlogaddlem  26877  atanlogsublem  26879  atanlogsub  26880  atantan  26887  atanbndlem  26889  atans2  26895  leibpi  26906  scvxcvx  26949  jensenlem2  26951  emcllem7  26965  basellem1  27044  ppisval  27067  chtdif  27121  ppidif  27126  ppiub  27167  chtublem  27174  chtub  27175  lgsdilem2  27296  gausslemma2dlem1a  27328  gausslemma2dlem2  27330  gausslemma2dlem5  27334  gausslemma2dlem6  27335  lgsquadlem1  27343  lgsquadlem2  27344  lgsquadlem3  27345  2lgslem1  27357  2sqlem3  27383  chebbnd1lem1  27432  chebbnd1lem2  27433  chebbnd1lem3  27434  dchrisumlem2  27453  dchrvmasumlem2  27461  dchrvmasumiflem1  27464  dchrisum0flblem2  27472  mulog2sumlem2  27498  logdivbnd  27519  pntpbnd2  27550  pntibndlem1  27552  pntibnd  27556  pntlemc  27558  pntlemg  27561  pntlemq  27564  pntlemf  27568  padicabvf  27594  padicabvcxp  27595  ostth2  27600  noextend  27630  noextendseq  27631  nosupno  27667  noinfno  27682  ttgcontlem1  28953  axpaschlem  29009  nbgr2vtx1edg  29419  nbuhgr2vtx1edgb  29421  cusgrexi  29512  structtocusgr  29515  pthdadjvtx  29796  pthdlem1  29834  pthd  29837  crctcshwlkn0lem3  29880  crctcshwlkn0lem4  29881  crctcshwlkn0lem5  29882  crctcshwlkn0lem7  29884  wlkiswwlks1  29935  wwlksm1edg  29949  wwlksnred  29960  wwlksnredwwlkn  29963  wwlksnextproplem3  29979  clwlkclwwlklem2fv1  30065  clwlkclwwlklem2fv2  30066  clwlkclwwlklem2a  30068  clwlkclwwlklem2  30070  clwwisshclwwslemlem  30083  clwwisshclwwslem  30084  erclwwlkref  30090  clwwlkel  30116  clwwlkf  30117  wwlksext2clwwlk  30127  wwlksubclwwlk  30128  umgr2cwwkdifex  30135  1pthd  30213  eucrctshift  30313  dlwwlknondlwlknonf1olem1  30434  numclwlk2lem2f  30447  frgrreggt1  30463  grpoinvf  30603  strlem3a  32323  hstrlem3a  32331  iundisj2f  32660  fcoinver  32674  fresf1o  32704  ssnnssfz  32860  bcm1n  32868  iundisj2fi  32870  fsumrp0cl  33081  cycpmco2lem6  33192  fxpsdrg  33236  lmodslmd  33265  fldgensdrg  33375  intlidl  33480  idlinsubrg  33491  rhmimaidl  33492  ssdifidllem  33516  ssmxidllem  33533  1arithidomlem1  33595  1arithidomlem2  33596  1arithidom  33597  fldextsdrg  33798  fldextrspunlem2  33821  fldextrspundgdvdslem  33824  fldextrspundgdvds  33825  minplyirred  33855  algextdeglem4  33864  algextdeglem8  33868  rtelextdg2lem  33870  constrsdrg  33919  2sqr3minply  33924  cos9thpiminply  33932  locfinreflem  33984  locfinref  33985  xrge0iifcnv  34077  xrge0iifiso  34079  xrge0iifhom  34081  esumc  34195  esumle  34202  esumlef  34206  esumpinfsum  34221  esumpcvgval  34222  fiunelros  34318  voliune  34373  volfiniune  34374  sibfinima  34483  eulerpartlemt  34515  fiblem  34542  fibp1  34545  dstrvprob  34616  ballotlemsel1i  34657  ballotlemfrceq  34673  plymulx0  34691  signstfvc  34718  signstfveq0  34721  bnj944  35080  bnj998  35099  bnj1136  35139  bnj1408  35178  erdszelem4  35376  erdszelem8  35380  txsconnlem  35422  cvxsconn  35425  cvmliftpht  35500  snmlff  35511  elmrsubrn  35702  msrf  35724  mthmpps  35764  sinccvglem  35854  trer  36498  poimirlem6  37947  poimirlem7  37948  poimirlem9  37950  poimirlem17  37958  poimirlem20  37961  poimirlem28  37969  poimirlem29  37970  poimirlem30  37971  poimirlem31  37972  poimirlem32  37973  areacirc  38034  nnubfi  38071  prter1  39325  lkrlss  39541  diaf11N  41495  dibf11N  41607  lclkr  41979  lclkrs  41985  lcfrlem9  41996  lcfr  42031  mapd1o  42094  hdmapf1oN  42311  hgmapf1oN  42349  frlmvscadiccat  42951  fimgmcyc  42979  nacsfix  43144  eldioph2lem1  43192  irrapxlem1  43250  rmxypairf1o  43339  jm2.27a  43433  hbtlem2  43552  hbt  43558  mon1psubm  43627  onnoxpg  43856  pren2d  43983  binomcxplemnotnn0  44783  elixpconstg  45519  elfzfzo  45710  monoords  45730  eluzd  45837  fmul01lt1lem2  46015  sumnnodd  46060  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  iblsplit  46394  iblspltprt  46401  itgspltprt  46407  stoweidlem11  46439  stoweidlem17  46445  fourierdlem12  46547  fourierdlem20  46555  fourierdlem25  46560  fourierdlem37  46572  fourierdlem41  46576  fourierdlem48  46582  fourierdlem49  46583  fourierdlem50  46584  fourierdlem54  46588  fourierdlem64  46598  fourierdlem73  46607  fourierdlem79  46613  fourierdlem102  46636  fourierdlem111  46645  fourierdlem114  46648  etransclem23  46685  etransclem48  46710  ormkglobd  47305  chnsubseq  47310  2elfz2melfz  47766  elfzlble  47768  ceilhalfelfzo1  47782  1elfzo1ceilhalf1  47789  difltmodne  47796  modm2nep1  47820  modm1nep2  47822  modm1p1ne  47824  iccpartiltu  47882  iccpartigtl  47883  iccpartlt  47884  iccpartgt  47887  lswn0  47904  fmtnoge3  47993  fmtnodvds  48007  odz2prm2pw  48026  fmtnole4prm  48041  lighneallem4b  48072  nprmdvdsfacm1lem3  48085  nprmdvdsfacm1lem4  48086  nprmdvdsfacm1  48087  mogoldbb  48261  nnsum4primesevenALTV  48277  bgoldbtbndlem3  48283  gpgprismgriedgdmss  48528  gpgprismgrusgra  48534  gpg3nbgrvtx0  48552  gpg3nbgrvtx0ALT  48553  gpg5nbgrvtx03star  48556  gpg5nbgr3star  48557  gpg3kgrtriexlem3  48561  gpg3kgrtriexlem4  48562  gpg3kgrtriexlem6  48564  gpgprismgr4cycllem3  48573  gpgprismgr4cycllem9  48579  ssnn0ssfz  48825  lmod1  48968  elfzolborelfzop1  48995  nnolog2flm1  49066  funcf2lem2  49557  isnatd  49698