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  7305  limuni3  7831  onfununi  8313  smores2  8326  smoiso  8334  oelimcl  8567  iserd  8700  resixp  8909  undifixp  8910  alephval3  10070  canthwelem  10610  canthwe  10611  r1limwun  10696  wunex2  10698  tskcard  10741  gruina  10778  eluzmn  12807  eluzuzle  12809  uztrn  12818  eluzadd  12829  eluzsub  12830  subeluzsub  12837  nn0pzuz  12871  zsupss  12903  nn0ge2m1nnALT  12908  xov1plusxeqvd  13466  ige2m1fz  13585  0elfz  13592  uzsubfz0  13604  elfzmlbm  13606  difelfzle  13609  difelfznle  13610  fvffz0  13614  elfzolt2b  13638  elfzolt3b  13639  elfzouz2  13642  fzossrbm1  13656  elfzo0  13668  eluzgtdifelfzo  13695  elfzodifsumelfzo  13699  fzonn0p1  13710  fzonn0p1p1  13712  fzo0sn0fzo1  13723  ssfzo12bi  13729  fzoopth  13730  ubmelm1fzo  13731  elfzonelfzo  13737  fzosplitprm1  13745  fzostep1  13751  fvinim0ffz  13754  flword2  13782  uzsup  13832  modfzo0difsn  13915  modsumfzodifsn  13916  fsuppmapnn0fiub  13963  suppssfz  13966  1elfz0hash  14362  fzsdom2  14400  ccatrn  14561  ccat2s1fvw  14610  pfxn0  14658  pfxtrcfv0  14666  pfxtrcfvl  14669  swrdswrd  14677  swrdccatin1  14697  pfxccat3  14706  pfxccat3a  14710  repswswrd  14756  cshwidxmod  14775  cshw1  14794  cshwcsh2id  14801  swrds2  14913  pfx2  14920  2swrd2eqwrdeq  14926  ccat2s1fvwALT  14928  rexuzre  15326  limsupgre  15454  rlimclim1  15518  rlimclim  15519  climrlim2  15520  isercolllem1  15638  isercoll  15641  climcndslem1  15822  fallfacval4  16016  tanhbnd  16136  sinbnd2  16157  cosbnd2  16158  rpnnen2lem12  16200  nn0o  16360  bitsfzolem  16411  bitsfzo  16412  bitsmod  16413  bitsfi  16414  bitsinv1lem  16418  bitsinv1  16419  smueqlem  16467  dvdsnprmd  16667  2mulprm  16670  hashgcdlem  16765  prm23lt5  16792  zgz  16911  gznegcl  16913  gzcjcl  16914  gzaddcl  16915  gzmulcl  16916  vdwlem9  16967  prmgaplem3  17031  prmgaplem4  17032  cshwshashlem2  17074  setsstruct2  17151  ismred  17570  isfuncd  17834  homdmcoa  18036  isdrs2  18274  fpwipodrs  18506  ipodrsima  18507  sgrp2rid2ex  18861  subgid  19067  issubg2  19080  subsubg  19088  gaorber  19247  orbsta  19252  pmtrfconj  19403  psgnunilem2  19432  psgnunilem3  19433  psgnunilem4  19434  pgpfi1  19532  subgpgp  19534  pgpssslw  19551  subgslw  19553  sylow2alem2  19555  fislw  19562  sylow3lem3  19566  efgs1  19672  efgsp1  19674  efgsres  19675  efgredleme  19680  efgcpbllemb  19692  lt6abl  19832  telgsumfzs  19926  ablfac1eu  20012  isrngd  20089  prdsrngd  20092  ringrng  20201  isringrng  20203  isringd  20207  ringsrg  20213  ring1  20226  prdsringd  20237  subrngid  20465  subrngsubg  20468  issubrng2  20474  subsubrng  20479  subrgsubg  20493  subrgsubrng  20494  sdrgid  20708  cntzsdrg  20718  subdrgint  20719  sdrgint  20720  islmodd  20779  islssd  20848  islss4  20875  dflidl2rng  21135  rnglidl0  21146  rnglidl1  21149  rnglidlrng  21164  rng2idlsubrng  21182  rhmpreimaidl  21194  gzrngunit  21357  expmhm  21360  zringunit  21383  prmirredlem  21389  znidomb  21478  isphld  21570  ocvocv  21587  ocvlss  21588  frlmlbs  21713  psdmul  22060  gsummoncoe1  22202  mp2pm2mplem4  22703  chfacfisf  22748  chfacfisfcpmat  22749  chfacfscmulfsupp  22753  chfacfpmmulfsupp  22757  chfacfpmmulgsum2  22759  2ndcctbss  23349  finlocfin  23414  dissnlocfin  23423  locfindis  23424  locfincf  23425  isfild  23752  infil  23757  neifil  23774  flimfcls  23920  istgp2  23985  oppgtmd  23991  oppgtgp  23992  distgp  23993  indistgp  23994  efmndtmd  23995  submtmd  23998  subgtgp  23999  symgtgp  24000  qustgplem  24015  prdstmdd  24018  prdstgpd  24019  tlmtgp  24090  isngp4  24507  subgngp  24530  ngptgp  24531  tngngp2  24547  nrgtrg  24585  nrgtdrg  24588  elii2  24839  icopnfcnv  24847  xrhmeo  24851  lebnumii  24872  phtpcer  24901  reparpht  24905  phtpcco2  24906  pcohtpy  24927  pcoass  24931  pcorevlem  24933  isclmi  24984  isncvsngpd  25057  cphsubrglem  25084  cphclm  25096  phclm  25139  tcphcph  25144  clsocv  25157  cphsscph  25158  cmslssbn  25279  pjthlem2  25345  ovolf  25390  iundisj2  25457  vitalilem2  25517  vitali  25521  itg2monolem3  25660  dvfsumlem1  25939  dvfsumlem3  25942  mon1puc1p  26063  uc1pmon1p  26064  mon1pid  26066  ply1remlem  26077  drnguc1p  26086  plyaddlem1  26125  coeidlem  26149  aannenlem2  26244  radcnvcl  26333  pilem2  26369  coseq00topi  26418  coseq0negpitopi  26419  tangtx  26421  tanabsge  26422  cosq14gt0  26426  cosq14ge0  26427  cosq34lt1  26443  cosordlem  26446  cos0pilt1  26448  sinord  26450  resinf1o  26452  tanord1  26453  tanord  26454  efif1olem3  26460  efsubm  26467  relogrn  26477  logimclad  26488  logrnaddcl  26490  logneg  26504  logcj  26522  argregt0  26526  argrege0  26527  argimgt0  26528  argimlt0  26529  logimul  26530  logneg2  26531  logdmnrp  26557  logcnlem4  26561  dvloglem  26564  logf1o2  26566  efopnlem2  26573  cxpsqrtlem  26618  relogbval  26689  nnlogbexp  26698  relogbcxp  26702  relogbcxpb  26704  logbgt0b  26710  asinneg  26803  asinsin  26809  acoscos  26810  acosbnd  26817  atancj  26827  atanlogaddlem  26830  atanlogsublem  26832  atanlogsub  26833  atantan  26840  atanbndlem  26842  atans2  26848  leibpi  26859  scvxcvx  26903  jensenlem2  26905  emcllem7  26919  basellem1  26998  ppisval  27021  chtdif  27075  ppidif  27080  ppiub  27122  chtublem  27129  chtub  27130  lgsdilem2  27251  gausslemma2dlem1a  27283  gausslemma2dlem2  27285  gausslemma2dlem5  27289  gausslemma2dlem6  27290  lgsquadlem1  27298  lgsquadlem2  27299  lgsquadlem3  27300  2lgslem1  27312  2sqlem3  27338  chebbnd1lem1  27387  chebbnd1lem2  27388  chebbnd1lem3  27389  dchrisumlem2  27408  dchrvmasumlem2  27416  dchrvmasumiflem1  27419  dchrisum0flblem2  27427  mulog2sumlem2  27453  logdivbnd  27474  pntpbnd2  27505  pntibndlem1  27507  pntibnd  27511  pntlemc  27513  pntlemg  27516  pntlemq  27519  pntlemf  27523  padicabvf  27549  padicabvcxp  27550  ostth2  27555  noextend  27585  noextendseq  27586  nosupno  27622  noinfno  27637  ttgcontlem1  28819  axpaschlem  28874  nbgr2vtx1edg  29284  nbuhgr2vtx1edgb  29286  cusgrexi  29377  structtocusgr  29380  pthdadjvtx  29665  pthdlem1  29703  pthd  29706  crctcshwlkn0lem3  29749  crctcshwlkn0lem4  29750  crctcshwlkn0lem5  29751  crctcshwlkn0lem7  29753  wlkiswwlks1  29804  wwlksm1edg  29818  wwlksnred  29829  wwlksnredwwlkn  29832  wwlksnextproplem3  29848  clwlkclwwlklem2fv1  29931  clwlkclwwlklem2fv2  29932  clwlkclwwlklem2a  29934  clwlkclwwlklem2  29936  clwwisshclwwslemlem  29949  clwwisshclwwslem  29950  erclwwlkref  29956  clwwlkel  29982  clwwlkf  29983  wwlksext2clwwlk  29993  wwlksubclwwlk  29994  umgr2cwwkdifex  30001  1pthd  30079  eucrctshift  30179  dlwwlknondlwlknonf1olem1  30300  numclwlk2lem2f  30313  frgrreggt1  30329  grpoinvf  30468  strlem3a  32188  hstrlem3a  32196  iundisj2f  32526  fcoinver  32540  fresf1o  32562  ssnnssfz  32717  bcm1n  32725  iundisj2fi  32727  ccatdmss  32878  chnub  32945  chnso  32947  fsumrp0cl  32969  submomnd  33031  cycpmco2lem6  33095  lmodslmd  33164  fldgensdrg  33271  suborng  33300  intlidl  33398  idlinsubrg  33409  rhmimaidl  33410  ssdifidllem  33434  ssmxidllem  33451  1arithidomlem1  33513  1arithidomlem2  33514  1arithidom  33515  fldextsdrg  33657  fldextrspunlem2  33679  fldextrspundgdvdslem  33682  fldextrspundgdvds  33683  minplyirred  33708  algextdeglem4  33717  algextdeglem8  33721  rtelextdg2lem  33723  constrsdrg  33772  2sqr3minply  33777  cos9thpiminply  33785  locfinreflem  33837  locfinref  33838  xrge0iifcnv  33930  xrge0iifiso  33932  xrge0iifhom  33934  esumc  34048  esumle  34055  esumlef  34059  esumpinfsum  34074  esumpcvgval  34075  fiunelros  34171  voliune  34226  volfiniune  34227  sibfinima  34337  eulerpartlemt  34369  fiblem  34396  fibp1  34399  dstrvprob  34470  ballotlemsel1i  34511  ballotlemfrceq  34527  plymulx0  34545  signstfvc  34572  signstfveq0  34575  bnj944  34935  bnj998  34954  bnj1136  34994  bnj1408  35033  erdszelem4  35188  erdszelem8  35192  txsconnlem  35234  cvxsconn  35237  cvmliftpht  35312  snmlff  35323  elmrsubrn  35514  msrf  35536  mthmpps  35576  sinccvglem  35666  trer  36311  poimirlem6  37627  poimirlem7  37628  poimirlem9  37630  poimirlem17  37638  poimirlem20  37641  poimirlem28  37649  poimirlem29  37650  poimirlem30  37651  poimirlem31  37652  poimirlem32  37653  areacirc  37714  nnubfi  37751  prter1  38879  lkrlss  39095  diaf11N  41050  dibf11N  41162  lclkr  41534  lclkrs  41540  lcfrlem9  41551  lcfr  41586  mapd1o  41649  hdmapf1oN  41866  hgmapf1oN  41904  frlmvscadiccat  42501  fimgmcyc  42529  nacsfix  42707  eldioph2lem1  42755  irrapxlem1  42817  rmxypairf1o  42907  jm2.27a  43001  hbtlem2  43120  hbt  43126  mon1psubm  43195  onnog  43425  pren2d  43552  binomcxplemnotnn0  44352  elixpconstg  45090  elfzfzo  45282  monoords  45302  elfzod  45403  eluzd  45412  fmul01lt1lem2  45590  sumnnodd  45635  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  iblsplit  45971  iblspltprt  45978  itgspltprt  45984  stoweidlem11  46016  stoweidlem17  46022  fourierdlem12  46124  fourierdlem20  46132  fourierdlem25  46137  fourierdlem37  46149  fourierdlem41  46153  fourierdlem48  46159  fourierdlem49  46160  fourierdlem50  46161  fourierdlem54  46165  fourierdlem64  46175  fourierdlem73  46184  fourierdlem79  46190  fourierdlem102  46213  fourierdlem111  46222  fourierdlem114  46225  etransclem23  46262  etransclem48  46287  ormkglobd  46880  2elfz2melfz  47323  elfzlble  47325  ceilhalfelfzo1  47335  1elfzo1ceilhalf1  47342  difltmodne  47347  modm2nep1  47371  modm1nep2  47373  modm1p1ne  47375  iccpartiltu  47427  iccpartigtl  47428  iccpartlt  47429  iccpartgt  47432  lswn0  47449  fmtnoge3  47535  fmtnodvds  47549  odz2prm2pw  47568  fmtnole4prm  47583  lighneallem4b  47614  mogoldbb  47790  nnsum4primesevenALTV  47806  bgoldbtbndlem3  47812  grlimgrtrilem1  47997  gpgprismgriedgdmss  48047  gpgprismgrusgra  48053  gpg3nbgrvtx0  48071  gpg3nbgrvtx0ALT  48072  gpg5nbgrvtx03star  48075  gpg5nbgr3star  48076  gpg3kgrtriexlem3  48080  gpg3kgrtriexlem4  48081  gpg3kgrtriexlem6  48083  gpgprismgr4cycllem3  48091  gpgprismgr4cycllem9  48097  ssnn0ssfz  48341  lmod1  48485  elfzolborelfzop1  48512  nnolog2flm1  48583  funcf2lem2  49075  isnatd  49216