Theorem syl3anbrc 1343

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 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  7363  limuni3  7889  onfununi  8397  smores2  8410  smoiso  8418  oelimcl  8656  iserd  8789  resixp  8991  undifixp  8992  alephval3  10179  canthwelem  10719  canthwe  10720  r1limwun  10805  wunex2  10807  tskcard  10850  gruina  10887  eluzmn  12910  eluzuzle  12912  uztrn  12921  eluzadd  12932  eluzsub  12933  subeluzsub  12940  nn0pzuz  12970  zsupss  13002  nn0ge2m1nnALT  13007  xov1plusxeqvd  13558  ige2m1fz  13674  0elfz  13681  uzsubfz0  13693  elfzmlbm  13695  difelfzle  13698  difelfznle  13699  fvffz0  13703  elfzolt2b  13727  elfzolt3b  13728  elfzouz2  13731  fzossrbm1  13745  elfzo0  13757  eluzgtdifelfzo  13778  elfzodifsumelfzo  13782  fzonn0p1  13793  fzonn0p1p1  13795  fzo0sn0fzo1  13805  ssfzo12bi  13811  fzoopth  13812  ubmelm1fzo  13813  elfzonelfzo  13819  fzosplitprm1  13827  fzostep1  13833  fvinim0ffz  13836  flword2  13864  uzsup  13914  modfzo0difsn  13994  modsumfzodifsn  13995  fsuppmapnn0fiub  14042  suppssfz  14045  1elfz0hash  14439  fzsdom2  14477  ccatrn  14637  ccat2s1fvw  14686  pfxn0  14734  pfxtrcfv0  14742  pfxtrcfvl  14745  swrdswrd  14753  swrdccatin1  14773  pfxccat3  14782  pfxccat3a  14786  repswswrd  14832  cshwidxmod  14851  cshw1  14870  cshwcsh2id  14877  swrds2  14989  pfx2  14996  2swrd2eqwrdeq  15002  ccat2s1fvwALT  15004  rexuzre  15401  limsupgre  15527  rlimclim1  15591  rlimclim  15592  climrlim2  15593  isercolllem1  15713  isercoll  15716  climcndslem1  15897  fallfacval4  16091  tanhbnd  16209  sinbnd2  16230  cosbnd2  16231  rpnnen2lem12  16273  nn0o  16431  bitsfzolem  16480  bitsfzo  16481  bitsmod  16482  bitsfi  16483  bitsinv1lem  16487  bitsinv1  16488  smueqlem  16536  dvdsnprmd  16737  2mulprm  16740  hashgcdlem  16835  prm23lt5  16861  zgz  16980  gznegcl  16982  gzcjcl  16983  gzaddcl  16984  gzmulcl  16985  vdwlem9  17036  prmgaplem3  17100  prmgaplem4  17101  cshwshashlem2  17144  setsstruct2  17221  ismred  17660  isfuncd  17929  homdmcoa  18134  isdrs2  18376  fpwipodrs  18610  ipodrsima  18611  sgrp2rid2ex  18962  subgid  19168  issubg2  19181  subsubg  19189  gaorber  19348  orbsta  19353  pmtrfconj  19508  psgnunilem2  19537  psgnunilem3  19538  psgnunilem4  19539  pgpfi1  19637  subgpgp  19639  pgpssslw  19656  subgslw  19658  sylow2alem2  19660  fislw  19667  sylow3lem3  19671  efgs1  19777  efgsp1  19779  efgsres  19780  efgredleme  19785  efgcpbllemb  19797  lt6abl  19937  telgsumfzs  20031  ablfac1eu  20117  isrngd  20200  prdsrngd  20203  ringrng  20308  isringrng  20310  isringd  20314  ringsrg  20320  ring1  20333  prdsringd  20344  subrngid  20575  subrngsubg  20578  issubrng2  20584  subsubrng  20589  subrgsubg  20605  subrgsubrng  20606  sdrgid  20815  cntzsdrg  20825  subdrgint  20826  sdrgint  20827  islmodd  20886  islssd  20956  islss4  20983  dflidl2rng  21251  rnglidl0  21262  rnglidl1  21265  rnglidlrng  21280  rng2idlsubrng  21298  rhmpreimaidl  21310  gzrngunit  21474  expmhm  21477  zringunit  21500  prmirredlem  21506  znidomb  21603  isphld  21695  ocvocv  21712  ocvlss  21713  frlmlbs  21840  psdmul  22193  gsummoncoe1  22333  mp2pm2mplem4  22836  chfacfisf  22881  chfacfisfcpmat  22882  chfacfscmulfsupp  22886  chfacfpmmulfsupp  22890  chfacfpmmulgsum2  22892  2ndcctbss  23484  finlocfin  23549  dissnlocfin  23558  locfindis  23559  locfincf  23560  isfild  23887  infil  23892  neifil  23909  flimfcls  24055  istgp2  24120  oppgtmd  24126  oppgtgp  24127  distgp  24128  indistgp  24129  efmndtmd  24130  submtmd  24133  subgtgp  24134  symgtgp  24135  qustgplem  24150  prdstmdd  24153  prdstgpd  24154  tlmtgp  24225  isngp4  24646  subgngp  24669  ngptgp  24670  tngngp2  24694  nrgtrg  24732  nrgtdrg  24735  elii2  24984  icopnfcnv  24992  xrhmeo  24996  lebnumii  25017  phtpcer  25046  reparpht  25050  phtpcco2  25051  pcohtpy  25072  pcoass  25076  pcorevlem  25078  isclmi  25129  isncvsngpd  25203  cphsubrglem  25230  cphclm  25242  phclm  25285  tcphcph  25290  clsocv  25303  cphsscph  25304  cmslssbn  25425  pjthlem2  25491  ovolf  25536  iundisj2  25603  vitalilem2  25663  vitali  25667  itg2monolem3  25807  dvfsumlem1  26086  dvfsumlem3  26089  mon1puc1p  26210  uc1pmon1p  26211  mon1pid  26213  ply1remlem  26224  drnguc1p  26233  plyaddlem1  26272  coeidlem  26296  aannenlem2  26389  radcnvcl  26478  pilem2  26514  coseq00topi  26562  coseq0negpitopi  26563  tangtx  26565  tanabsge  26566  cosq14gt0  26570  cosq14ge0  26571  cosq34lt1  26587  cosordlem  26590  cos0pilt1  26592  sinord  26594  resinf1o  26596  tanord1  26597  tanord  26598  efif1olem3  26604  efsubm  26611  relogrn  26621  logimclad  26632  logrnaddcl  26634  logneg  26648  logcj  26666  argregt0  26670  argrege0  26671  argimgt0  26672  argimlt0  26673  logimul  26674  logneg2  26675  logdmnrp  26701  logcnlem4  26705  dvloglem  26708  logf1o2  26710  efopnlem2  26717  cxpsqrtlem  26762  relogbval  26833  nnlogbexp  26842  relogbcxp  26846  relogbcxpb  26848  logbgt0b  26854  asinneg  26947  asinsin  26953  acoscos  26954  acosbnd  26961  atancj  26971  atanlogaddlem  26974  atanlogsublem  26976  atanlogsub  26977  atantan  26984  atanbndlem  26986  atans2  26992  leibpi  27003  scvxcvx  27047  jensenlem2  27049  emcllem7  27063  basellem1  27142  ppisval  27165  chtdif  27219  ppidif  27224  ppiub  27266  chtublem  27273  chtub  27274  lgsdilem2  27395  gausslemma2dlem1a  27427  gausslemma2dlem2  27429  gausslemma2dlem5  27433  gausslemma2dlem6  27434  lgsquadlem1  27442  lgsquadlem2  27443  lgsquadlem3  27444  2lgslem1  27456  2sqlem3  27482  chebbnd1lem1  27531  chebbnd1lem2  27532  chebbnd1lem3  27533  dchrisumlem2  27552  dchrvmasumlem2  27560  dchrvmasumiflem1  27563  dchrisum0flblem2  27571  mulog2sumlem2  27597  logdivbnd  27618  pntpbnd2  27649  pntibndlem1  27651  pntibnd  27655  pntlemc  27657  pntlemg  27660  pntlemq  27663  pntlemf  27667  padicabvf  27693  padicabvcxp  27694  ostth2  27699  noextend  27729  noextendseq  27730  nosupno  27766  noinfno  27781  ttgcontlem1  28917  axpaschlem  28973  nbgr2vtx1edg  29385  nbuhgr2vtx1edgb  29387  cusgrexi  29478  structtocusgr  29481  pthdadjvtx  29766  pthdlem1  29802  pthd  29805  crctcshwlkn0lem3  29845  crctcshwlkn0lem4  29846  crctcshwlkn0lem5  29847  crctcshwlkn0lem7  29849  wlkiswwlks1  29900  wwlksm1edg  29914  wwlksnred  29925  wwlksnredwwlkn  29928  wwlksnextproplem3  29944  clwlkclwwlklem2fv1  30027  clwlkclwwlklem2fv2  30028  clwlkclwwlklem2a  30030  clwlkclwwlklem2  30032  clwwisshclwwslemlem  30045  clwwisshclwwslem  30046  erclwwlkref  30052  clwwlkel  30078  clwwlkf  30079  wwlksext2clwwlk  30089  wwlksubclwwlk  30090  umgr2cwwkdifex  30097  1pthd  30175  eucrctshift  30275  dlwwlknondlwlknonf1olem1  30396  numclwlk2lem2f  30409  frgrreggt1  30425  grpoinvf  30564  strlem3a  32284  hstrlem3a  32292  iundisj2f  32612  fcoinver  32626  fresf1o  32650  ssnnssfz  32792  bcm1n  32800  iundisj2fi  32802  ccatdmss  32916  chnub  32984  chnso  32986  fsumrp0cl  33007  submomnd  33060  cycpmco2lem6  33124  lmodslmd  33183  fldgensdrg  33281  suborng  33310  intlidl  33413  idlinsubrg  33424  rhmimaidl  33425  ssdifidllem  33449  ssmxidllem  33466  1arithidomlem1  33528  1arithidomlem2  33529  1arithidom  33530  minplyirred  33704  algextdeglem4  33711  algextdeglem8  33715  rtelextdg2lem  33717  2sqr3minply  33738  locfinreflem  33786  locfinref  33787  xrge0iifcnv  33879  xrge0iifiso  33881  xrge0iifhom  33883  esumc  34015  esumle  34022  esumlef  34026  esumpinfsum  34041  esumpcvgval  34042  fiunelros  34138  voliune  34193  volfiniune  34194  sibfinima  34304  eulerpartlemt  34336  fiblem  34363  fibp1  34366  dstrvprob  34436  ballotlemsel1i  34477  ballotlemfrceq  34493  plymulx0  34524  signstfvc  34551  signstfveq0  34554  bnj944  34914  bnj998  34933  bnj1136  34973  bnj1408  35012  erdszelem4  35162  erdszelem8  35166  txsconnlem  35208  cvxsconn  35211  cvmliftpht  35286  snmlff  35297  elmrsubrn  35488  msrf  35510  mthmpps  35550  sinccvglem  35640  trer  36282  poimirlem6  37586  poimirlem7  37587  poimirlem9  37589  poimirlem17  37597  poimirlem20  37600  poimirlem28  37608  poimirlem29  37609  poimirlem30  37610  poimirlem31  37611  poimirlem32  37612  areacirc  37673  nnubfi  37710  prter1  38835  lkrlss  39051  diaf11N  41006  dibf11N  41118  lclkr  41490  lclkrs  41496  lcfrlem9  41507  lcfr  41542  mapd1o  41605  hdmapf1oN  41822  hgmapf1oN  41860  sn-inelr  42443  frlmvscadiccat  42461  fimgmcyc  42489  nacsfix  42668  eldioph2lem1  42716  irrapxlem1  42778  rmxypairf1o  42868  jm2.27a  42962  hbtlem2  43081  hbt  43087  mon1psubm  43160  onnog  43391  pren2d  43518  binomcxplemnotnn0  44325  elixpconstg  44991  elfzfzo  45191  monoords  45212  elfzod  45315  eluzd  45324  fmul01lt1lem2  45506  sumnnodd  45551  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  iblsplit  45887  iblspltprt  45894  itgspltprt  45900  stoweidlem11  45932  stoweidlem17  45938  fourierdlem12  46040  fourierdlem20  46048  fourierdlem25  46053  fourierdlem37  46065  fourierdlem41  46069  fourierdlem48  46075  fourierdlem49  46076  fourierdlem50  46077  fourierdlem54  46081  fourierdlem64  46091  fourierdlem73  46100  fourierdlem79  46106  fourierdlem102  46129  fourierdlem111  46138  fourierdlem114  46141  etransclem23  46178  etransclem48  46203  2elfz2melfz  47233  elfzlble  47235  iccpartiltu  47296  iccpartigtl  47297  iccpartlt  47298  iccpartgt  47301  lswn0  47318  fmtnoge3  47404  fmtnodvds  47418  odz2prm2pw  47437  fmtnole4prm  47452  lighneallem4b  47483  mogoldbb  47659  nnsum4primesevenALTV  47675  bgoldbtbndlem3  47681  grlimgrtrilem1  47818  ssnn0ssfz  48074  lmod1  48221  elfzolborelfzop1  48248  nnolog2flm1  48324