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 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  7346  limuni3  7872  onfununi  8379  smores2  8392  smoiso  8400  oelimcl  8636  iserd  8769  resixp  8971  undifixp  8972  alephval3  10147  canthwelem  10687  canthwe  10688  r1limwun  10773  wunex2  10775  tskcard  10818  gruina  10855  eluzmn  12882  eluzuzle  12884  uztrn  12893  eluzadd  12904  eluzsub  12905  subeluzsub  12912  nn0pzuz  12944  zsupss  12976  nn0ge2m1nnALT  12981  xov1plusxeqvd  13534  ige2m1fz  13653  0elfz  13660  uzsubfz0  13672  elfzmlbm  13674  difelfzle  13677  difelfznle  13678  fvffz0  13682  elfzolt2b  13706  elfzolt3b  13707  elfzouz2  13710  fzossrbm1  13724  elfzo0  13736  eluzgtdifelfzo  13762  elfzodifsumelfzo  13766  fzonn0p1  13777  fzonn0p1p1  13779  fzo0sn0fzo1  13790  ssfzo12bi  13796  fzoopth  13797  ubmelm1fzo  13798  elfzonelfzo  13804  fzosplitprm1  13812  fzostep1  13818  fvinim0ffz  13821  flword2  13849  uzsup  13899  modfzo0difsn  13980  modsumfzodifsn  13981  fsuppmapnn0fiub  14028  suppssfz  14031  1elfz0hash  14425  fzsdom2  14463  ccatrn  14623  ccat2s1fvw  14672  pfxn0  14720  pfxtrcfv0  14728  pfxtrcfvl  14731  swrdswrd  14739  swrdccatin1  14759  pfxccat3  14768  pfxccat3a  14772  repswswrd  14818  cshwidxmod  14837  cshw1  14856  cshwcsh2id  14863  swrds2  14975  pfx2  14982  2swrd2eqwrdeq  14988  ccat2s1fvwALT  14990  rexuzre  15387  limsupgre  15513  rlimclim1  15577  rlimclim  15578  climrlim2  15579  isercolllem1  15697  isercoll  15700  climcndslem1  15881  fallfacval4  16075  tanhbnd  16193  sinbnd2  16214  cosbnd2  16215  rpnnen2lem12  16257  nn0o  16416  bitsfzolem  16467  bitsfzo  16468  bitsmod  16469  bitsfi  16470  bitsinv1lem  16474  bitsinv1  16475  smueqlem  16523  dvdsnprmd  16723  2mulprm  16726  hashgcdlem  16821  prm23lt5  16847  zgz  16966  gznegcl  16968  gzcjcl  16969  gzaddcl  16970  gzmulcl  16971  vdwlem9  17022  prmgaplem3  17086  prmgaplem4  17087  cshwshashlem2  17130  setsstruct2  17207  ismred  17646  isfuncd  17915  homdmcoa  18120  isdrs2  18363  fpwipodrs  18597  ipodrsima  18598  sgrp2rid2ex  18952  subgid  19158  issubg2  19171  subsubg  19179  gaorber  19338  orbsta  19343  pmtrfconj  19498  psgnunilem2  19527  psgnunilem3  19528  psgnunilem4  19529  pgpfi1  19627  subgpgp  19629  pgpssslw  19646  subgslw  19648  sylow2alem2  19650  fislw  19657  sylow3lem3  19661  efgs1  19767  efgsp1  19769  efgsres  19770  efgredleme  19775  efgcpbllemb  19787  lt6abl  19927  telgsumfzs  20021  ablfac1eu  20107  isrngd  20190  prdsrngd  20193  ringrng  20298  isringrng  20300  isringd  20304  ringsrg  20310  ring1  20323  prdsringd  20334  subrngid  20565  subrngsubg  20568  issubrng2  20574  subsubrng  20579  subrgsubg  20593  subrgsubrng  20594  sdrgid  20809  cntzsdrg  20819  subdrgint  20820  sdrgint  20821  islmodd  20880  islssd  20950  islss4  20977  dflidl2rng  21245  rnglidl0  21256  rnglidl1  21259  rnglidlrng  21274  rng2idlsubrng  21292  rhmpreimaidl  21304  gzrngunit  21468  expmhm  21471  zringunit  21494  prmirredlem  21500  znidomb  21597  isphld  21689  ocvocv  21706  ocvlss  21707  frlmlbs  21834  psdmul  22187  gsummoncoe1  22327  mp2pm2mplem4  22830  chfacfisf  22875  chfacfisfcpmat  22876  chfacfscmulfsupp  22880  chfacfpmmulfsupp  22884  chfacfpmmulgsum2  22886  2ndcctbss  23478  finlocfin  23543  dissnlocfin  23552  locfindis  23553  locfincf  23554  isfild  23881  infil  23886  neifil  23903  flimfcls  24049  istgp2  24114  oppgtmd  24120  oppgtgp  24121  distgp  24122  indistgp  24123  efmndtmd  24124  submtmd  24127  subgtgp  24128  symgtgp  24129  qustgplem  24144  prdstmdd  24147  prdstgpd  24148  tlmtgp  24219  isngp4  24640  subgngp  24663  ngptgp  24664  tngngp2  24688  nrgtrg  24726  nrgtdrg  24729  elii2  24978  icopnfcnv  24986  xrhmeo  24990  lebnumii  25011  phtpcer  25040  reparpht  25044  phtpcco2  25045  pcohtpy  25066  pcoass  25070  pcorevlem  25072  isclmi  25123  isncvsngpd  25197  cphsubrglem  25224  cphclm  25236  phclm  25279  tcphcph  25284  clsocv  25297  cphsscph  25298  cmslssbn  25419  pjthlem2  25485  ovolf  25530  iundisj2  25597  vitalilem2  25657  vitali  25661  itg2monolem3  25801  dvfsumlem1  26080  dvfsumlem3  26083  mon1puc1p  26204  uc1pmon1p  26205  mon1pid  26207  ply1remlem  26218  drnguc1p  26227  plyaddlem1  26266  coeidlem  26290  aannenlem2  26385  radcnvcl  26474  pilem2  26510  coseq00topi  26558  coseq0negpitopi  26559  tangtx  26561  tanabsge  26562  cosq14gt0  26566  cosq14ge0  26567  cosq34lt1  26583  cosordlem  26586  cos0pilt1  26588  sinord  26590  resinf1o  26592  tanord1  26593  tanord  26594  efif1olem3  26600  efsubm  26607  relogrn  26617  logimclad  26628  logrnaddcl  26630  logneg  26644  logcj  26662  argregt0  26666  argrege0  26667  argimgt0  26668  argimlt0  26669  logimul  26670  logneg2  26671  logdmnrp  26697  logcnlem4  26701  dvloglem  26704  logf1o2  26706  efopnlem2  26713  cxpsqrtlem  26758  relogbval  26829  nnlogbexp  26838  relogbcxp  26842  relogbcxpb  26844  logbgt0b  26850  asinneg  26943  asinsin  26949  acoscos  26950  acosbnd  26957  atancj  26967  atanlogaddlem  26970  atanlogsublem  26972  atanlogsub  26973  atantan  26980  atanbndlem  26982  atans2  26988  leibpi  26999  scvxcvx  27043  jensenlem2  27045  emcllem7  27059  basellem1  27138  ppisval  27161  chtdif  27215  ppidif  27220  ppiub  27262  chtublem  27269  chtub  27270  lgsdilem2  27391  gausslemma2dlem1a  27423  gausslemma2dlem2  27425  gausslemma2dlem5  27429  gausslemma2dlem6  27430  lgsquadlem1  27438  lgsquadlem2  27439  lgsquadlem3  27440  2lgslem1  27452  2sqlem3  27478  chebbnd1lem1  27527  chebbnd1lem2  27528  chebbnd1lem3  27529  dchrisumlem2  27548  dchrvmasumlem2  27556  dchrvmasumiflem1  27559  dchrisum0flblem2  27567  mulog2sumlem2  27593  logdivbnd  27614  pntpbnd2  27645  pntibndlem1  27647  pntibnd  27651  pntlemc  27653  pntlemg  27656  pntlemq  27659  pntlemf  27663  padicabvf  27689  padicabvcxp  27690  ostth2  27695  noextend  27725  noextendseq  27726  nosupno  27762  noinfno  27777  ttgcontlem1  28913  axpaschlem  28969  nbgr2vtx1edg  29381  nbuhgr2vtx1edgb  29383  cusgrexi  29474  structtocusgr  29477  pthdadjvtx  29762  pthdlem1  29798  pthd  29801  crctcshwlkn0lem3  29841  crctcshwlkn0lem4  29842  crctcshwlkn0lem5  29843  crctcshwlkn0lem7  29845  wlkiswwlks1  29896  wwlksm1edg  29910  wwlksnred  29921  wwlksnredwwlkn  29924  wwlksnextproplem3  29940  clwlkclwwlklem2fv1  30023  clwlkclwwlklem2fv2  30024  clwlkclwwlklem2a  30026  clwlkclwwlklem2  30028  clwwisshclwwslemlem  30041  clwwisshclwwslem  30042  erclwwlkref  30048  clwwlkel  30074  clwwlkf  30075  wwlksext2clwwlk  30085  wwlksubclwwlk  30086  umgr2cwwkdifex  30093  1pthd  30171  eucrctshift  30271  dlwwlknondlwlknonf1olem1  30392  numclwlk2lem2f  30405  frgrreggt1  30421  grpoinvf  30560  strlem3a  32280  hstrlem3a  32288  iundisj2f  32609  fcoinver  32623  fresf1o  32647  ssnnssfz  32795  bcm1n  32802  iundisj2fi  32804  ccatdmss  32918  chnub  32985  chnso  32987  fsumrp0cl  33008  submomnd  33069  cycpmco2lem6  33133  lmodslmd  33192  fldgensdrg  33295  suborng  33324  intlidl  33427  idlinsubrg  33438  rhmimaidl  33439  ssdifidllem  33463  ssmxidllem  33480  1arithidomlem1  33542  1arithidomlem2  33543  1arithidom  33544  minplyirred  33718  algextdeglem4  33725  algextdeglem8  33729  rtelextdg2lem  33731  2sqr3minply  33752  locfinreflem  33800  locfinref  33801  xrge0iifcnv  33893  xrge0iifiso  33895  xrge0iifhom  33897  esumc  34031  esumle  34038  esumlef  34042  esumpinfsum  34057  esumpcvgval  34058  fiunelros  34154  voliune  34209  volfiniune  34210  sibfinima  34320  eulerpartlemt  34352  fiblem  34379  fibp1  34382  dstrvprob  34452  ballotlemsel1i  34493  ballotlemfrceq  34509  plymulx0  34540  signstfvc  34567  signstfveq0  34570  bnj944  34930  bnj998  34949  bnj1136  34989  bnj1408  35028  erdszelem4  35178  erdszelem8  35182  txsconnlem  35224  cvxsconn  35227  cvmliftpht  35302  snmlff  35313  elmrsubrn  35504  msrf  35526  mthmpps  35566  sinccvglem  35656  trer  36298  poimirlem6  37612  poimirlem7  37613  poimirlem9  37615  poimirlem17  37623  poimirlem20  37626  poimirlem28  37634  poimirlem29  37635  poimirlem30  37636  poimirlem31  37637  poimirlem32  37638  areacirc  37699  nnubfi  37736  prter1  38860  lkrlss  39076  diaf11N  41031  dibf11N  41143  lclkr  41515  lclkrs  41521  lcfrlem9  41532  lcfr  41567  mapd1o  41630  hdmapf1oN  41847  hgmapf1oN  41885  sn-inelr  42473  frlmvscadiccat  42492  fimgmcyc  42520  nacsfix  42699  eldioph2lem1  42747  irrapxlem1  42809  rmxypairf1o  42899  jm2.27a  42993  hbtlem2  43112  hbt  43118  mon1psubm  43187  onnog  43418  pren2d  43545  binomcxplemnotnn0  44351  elixpconstg  45028  elfzfzo  45226  monoords  45247  elfzod  45349  eluzd  45358  fmul01lt1lem2  45540  sumnnodd  45585  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  iblsplit  45921  iblspltprt  45928  itgspltprt  45934  stoweidlem11  45966  stoweidlem17  45972  fourierdlem12  46074  fourierdlem20  46082  fourierdlem25  46087  fourierdlem37  46099  fourierdlem41  46103  fourierdlem48  46109  fourierdlem49  46110  fourierdlem50  46111  fourierdlem54  46115  fourierdlem64  46125  fourierdlem73  46134  fourierdlem79  46140  fourierdlem102  46163  fourierdlem111  46172  fourierdlem114  46175  etransclem23  46212  etransclem48  46237  2elfz2melfz  47267  elfzlble  47269  difltmodne  47281  iccpartiltu  47346  iccpartigtl  47347  iccpartlt  47348  iccpartgt  47351  lswn0  47368  fmtnoge3  47454  fmtnodvds  47468  odz2prm2pw  47487  fmtnole4prm  47502  lighneallem4b  47533  mogoldbb  47709  nnsum4primesevenALTV  47725  bgoldbtbndlem3  47731  grlimgrtrilem1  47896  ceilhalfelfzo1  47950  gpg3nbgrvtx0  47966  gpg3nbgrvtx0ALT  47967  gpg5nbgrvtx03star  47970  gpg5nbgr3star  47971  ssnn0ssfz  48193  lmod1  48337  elfzolborelfzop1  48364  nnolog2flm1  48439