Theorem syl3anbrc 1362

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 1146	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
5		syl3anbrc.4	. 2 ⊢ (𝜏 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))
6	4, 5	sylibr 237	1 ⊢ (𝜑 → 𝜏)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  soisores  7327  limuni3  7852  onfununi  8333  smores2  8346  smoiso  8354  oelimcl  8593  iserd  8728  resixp  8945  undifixp  8946  alephval3  10170  canthwelem  10716  canthwe  10717  r1limwun  10802  wunex2  10804  tskcard  10847  gruina  10884  eluzmn  12953  eluzuzle  12955  uztrn  12964  eluzadd  12975  eluzsub  12976  subeluzsub  12979  nn0pzuz  13013  zsupss  13045  nn0ge2m1nnALT  13050  xov1plusxeqvd  13610  ige2m1fz  13731  0elfz  13738  uzsubfz0  13750  elfzmlbm  13752  difelfzle  13755  difelfznle  13756  fvffz0  13760  elfzod  13777  elfzolt2b  13785  elfzolt3b  13786  elfzouz2  13789  fzossrbm1  13803  elfzo0  13815  eluzgtdifelfzo  13842  elfzodifsumelfzo  13846  fzonn0p1  13857  fzonn0p1p1  13859  fzo0sn0fzo1  13870  ssfzo12bi  13876  fzoopth  13877  ubmelm1fzo  13878  elfzonelfzo  13884  fzosplitprm1  13893  fzostep1  13901  fvinim0ffz  13904  flword2  13933  uzsup  13983  modfzo0difsn  14066  modsumfzodifsn  14067  fsuppmapnn0fiub  14114  suppssfz  14117  1elfz0hash  14514  fzsdom2  14553  ccatdmss  14707  ccatrn  14715  ccat2s1fvw  14766  pfxn0  14816  pfxtrcfv0  14823  pfxtrcfvl  14826  swrdswrd  14834  swrdccatin1  14854  pfxccat3  14863  pfxccat3a  14867  repswswrd  14915  cshwidxmod  14934  cshw1  14953  cshwcsh2id  14959  swrds2  15071  pfx2  15078  2swrd2eqwrdeq  15086  ccat2s1fvwALT  15088  rexuzre  15500  limsupgre  15628  rlimclim1  15692  rlimclim  15693  climrlim2  15694  isercolllem1  15812  isercoll  15815  climcndslem1  15998  fallfacval4  16189  tanhbnd  16309  sinbnd2  16330  cosbnd2  16331  rpnnen2lem12  16373  nn0o  16533  bitsfzolem  16584  bitsfzo  16585  bitsmod  16586  bitsfi  16587  bitsinv1lem  16591  bitsinv1  16592  smueqlem  16640  dvdsnprmd  16845  2mulprm  16848  hashgcdlem  16945  prm23lt5  16972  zgz  17091  gznegcl  17093  gzcjcl  17094  gzaddcl  17095  gzmulcl  17096  vdwlem9  17147  prmgaplem3  17211  prmgaplem4  17212  cshwshashlem2  17254  setsstruct2  17332  ismred  17752  isfuncd  18020  homdmcoa  18222  isdrs2  18460  fpwipodrs  18694  ipodrsima  18695  chnub  18776  chnso  18778  sgrp2rid2ex  19106  subgid  19318  issubg2  19332  subsubg  19340  gaorber  19502  orbsta  19507  pmtrfconj  19660  psgnunilem2  19689  psgnunilem3  19690  psgnunilem4  19691  pgpfi1  19789  subgpgp  19791  pgpssslw  19808  subgslw  19810  sylow2alem2  19812  fislw  19819  sylow3lem3  19823  efgs1  19929  efgsp1  19931  efgsres  19932  efgredleme  19937  efgcpbllemb  19949  lt6abl  20089  telgsumfzs  20183  ablfac1eu  20269  submomnd  20326  isrngd  20375  prdsrngd  20378  ringrng  20494  isringrng  20496  isringd  20502  ringsrg  20508  ring1  20521  prdsringd  20530  subrngid  20781  subrngsubg  20784  issubrng2  20790  subsubrng  20795  subrgsubg  20809  subrgsubrng  20810  sdrgid  21029  cntzsdrg  21039  subdrgint  21040  sdrgint  21041  suborng  21113  islmodd  21121  islssd  21190  islss4  21217  dflidl2rng  21477  rnglidl0  21489  rnglidl1  21492  unichnlidl  21496  rnglidlrng  21515  rng2idlsubrng  21539  rhmpreimaidl  21551  ssdifidllem  21620  gzrngunit  21719  expmhm  21722  zringunit  21752  prmirredlem  21758  znidomb  21847  isphld  21940  ocvocv  21957  ocvlss  21958  frlmlbs  22083  psdmul  22467  gsummoncoe1  22606  mp2pm2mplem4  23107  chfacfisf  23152  chfacfisfcpmat  23153  chfacfscmulfsupp  23157  chfacfpmmulfsupp  23161  chfacfpmmulgsum2  23163  2ndcctbss  23754  finlocfin  23819  dissnlocfin  23828  locfindis  23829  locfincf  23830  isfild  24157  infil  24162  neifil  24179  flimfcls  24325  istgp2  24390  oppgtmd  24396  oppgtgp  24397  distgp  24398  indistgp  24399  efmndtmd  24400  submtmd  24403  subgtgp  24404  symgtgp  24405  qustgplem  24420  prdstmdd  24423  prdstgpd  24424  tlmtgp  24495  isngp4  24911  subgngp  24934  ngptgp  24935  tngngp2  24951  nrgtrg  24989  nrgtdrg  24992  elii2  25237  icopnfcnv  25243  xrhmeo  25247  lebnumii  25267  phtpcer  25296  reparpht  25299  phtpcco2  25300  pcohtpy  25321  pcoass  25325  pcorevlem  25327  isclmi  25378  isncvsngpd  25451  cphsubrglem  25478  cphclm  25490  phclm  25533  tcphcph  25538  clsocv  25551  cphsscph  25552  cmslssbn  25673  pjthlem2  25739  ovolf  25783  iundisj2  25850  vitalilem2  25910  vitali  25914  itg2monolem3  26053  dvfsumlem1  26326  dvfsumlem3  26328  mon1puc1p  26449  uc1pmon1p  26450  mon1pid  26452  ply1remlem  26463  drnguc1p  26472  plyaddlem1  26512  coeidlem  26536  plyn0mulidp  26584  aannenlem2  26638  radcnvcl  26726  pilem2  26761  coseq00topi  26813  coseq0negpitopi  26814  tangtx  26816  tanabsge  26817  cosq14gt0  26821  cosq14ge0  26822  cosq34lt1  26837  cosordlem  26840  cos0pilt1  26842  sinord  26844  resinf1o  26846  tanord1  26847  tanord  26848  efif1olem3  26854  efsubm  26861  relogrn  26871  logimclad  26882  logrnaddcl  26884  logneg  26898  logcj  26916  argregt0  26920  argrege0  26921  argimgt0  26922  argimlt0  26923  logimul  26924  logneg2  26925  logdmnrp  26951  logcnlem4  26955  dvloglem  26958  logf1o2  26960  efopnlem2  26967  cxpsqrtlem  27012  relogbval  27082  nnlogbexp  27091  relogbcxp  27095  relogbcxpb  27097  logbgt0b  27103  asinneg  27196  asinsin  27202  acoscos  27203  acosbnd  27210  atancj  27220  atanlogaddlem  27223  atanlogsublem  27225  atanlogsub  27226  atantan  27233  atanbndlem  27235  atans2  27241  leibpi  27252  scvxcvx  27295  jensenlem2  27297  emcllem7  27311  basellem1  27390  ppisval  27413  chtdif  27467  ppidif  27472  ppiub  27513  chtublem  27520  chtub  27521  lgsdilem2  27642  gausslemma2dlem1a  27674  gausslemma2dlem2  27676  gausslemma2dlem5  27680  gausslemma2dlem6  27681  lgsquadlem1  27689  lgsquadlem2  27690  lgsquadlem3  27691  2lgslem1  27703  2sqlem3  27729  chebbnd1lem1  27778  chebbnd1lem2  27779  chebbnd1lem3  27780  dchrisumlem2  27799  dchrvmasumlem2  27807  dchrvmasumiflem1  27810  dchrisum0flblem2  27818  mulog2sumlem2  27844  logdivbnd  27865  pntpbnd2  27896  pntibndlem1  27898  pntibnd  27902  pntlemc  27904  pntlemg  27907  pntlemq  27910  pntlemf  27914  padicabvf  27940  padicabvcxp  27941  ostth2  27946  fltoprmlem2  27976  noextend  28005  noextendseq  28006  nosupno  28042  noinfno  28057  ttgcontlem1  29444  axpaschlem  29500  nbgr2vtx1edg  29913  nbuhgr2vtx1edgb  29915  cusgrexi  30006  structtocusgr  30009  pthdadjvtx  30295  pthdlem1  30334  pthd  30337  crctcshwlkn0lem3  30383  crctcshwlkn0lem4  30384  crctcshwlkn0lem5  30385  crctcshwlkn0lem7  30387  wlkiswwlks1  30438  wwlksm1edg  30452  wwlksnred  30463  wwlksnredwwlkn  30466  wwlksnextproplem3  30482  clwlkclwwlklem2fv1  30568  clwlkclwwlklem2fv2  30569  clwlkclwwlklem2a  30571  clwlkclwwlklem2  30573  clwwisshclwwslemlem  30586  clwwisshclwwslem  30587  erclwwlkref  30593  clwwlkel  30619  clwwlkf  30620  wwlksext2clwwlk  30630  wwlksubclwwlk  30631  umgr2cwwkdifex  30638  1pthd  30716  eucrctshift  30826  dlwwlknondlwlknonf1olem1  30947  numclwlk2lem2f  30960  frgrreggt1  30976  grpoinvf  31116  strlem3a  32836  hstrlem3a  32844  iundisj2f  33166  fcoinver  33180  fresf1o  33207  ssnnssfz  33361  bcm1n  33369  iundisj2fi  33371  fsumrp0cl  33564  cycpmco2lem6  33674  fxpsdrg  33718  lmodslmd  33747  fldgensdrg  33858  intlidl  33952  idlinsubrg  33963  rhmimaidl  33964  ssmxidllem  33980  dflringlem2  34009  1arithidomlem1  34049  1arithidomlem2  34050  1arithidom  34051  fldextsdrg  34268  fldextrspunlem2  34291  fldextrspundgdvdslem  34294  fldextrspundgdvds  34295  minplyirred  34325  algextdeglem4  34334  algextdeglem8  34338  rtelextdg2lem  34340  constrsdrg  34389  2sqr3minply  34394  cos9thpiminply  34402  locfinreflem  34454  locfinref  34455  xrge0iifcnv  34547  xrge0iifiso  34549  xrge0iifhom  34551  esumc  34665  esumle  34672  esumlef  34676  esumpinfsum  34691  esumpcvgval  34692  fiunelros  34789  voliune  34844  volfiniune  34845  sibfinima  34954  eulerpartlemt  34986  fiblem  35013  fibp1  35016  dstrvprob  35087  ballotlemsel1i  35128  ballotlemfrceq  35144  signstfvc  35186  signstfveq0  35189  bnj944  35551  bnj998  35570  bnj1136  35610  bnj1408  35649  erdszelem4  35928  erdszelem8  35932  txsconnlem  35974  cvxsconn  35977  cvmliftpht  36052  snmlff  36063  elmrsubrn  36254  msrf  36276  mthmpps  36316  sinccvglem  36406  trer  37074  poimirlem6  38512  poimirlem7  38513  poimirlem9  38515  poimirlem17  38523  poimirlem20  38526  poimirlem28  38534  poimirlem29  38535  poimirlem30  38536  poimirlem31  38537  poimirlem32  38538  areacirc  38599  nnubfi  38652  prter1  39904  lkrlss  40120  diaf11N  42074  dibf11N  42186  lclkr  42558  lclkrs  42564  lcfrlem9  42575  lcfr  42610  mapd1o  42673  hdmapf1oN  42890  hgmapf1oN  42928  frlmvscadiccat  43538  fimgmcyc  43560  nacsfix  43676  eldioph2lem1  43724  irrapxlem1  43782  rmxypairf1o  43871  jm2.27a  43965  hbtlem2  44084  hbt  44090  mon1psubm  44159  onnoxpg  44388  pren2d  44515  binomcxplemnotnn0  45299  elixpconstg  46047  elfzfzo  46236  monoords  46256  eluzd  46363  fmul01lt1lem2  46541  sumnnodd  46586  ioodvbdlimc1lem2  46886  ioodvbdlimc2lem  46888  iblsplit  46920  iblspltprt  46927  itgspltprt  46933  stoweidlem11  46965  stoweidlem17  46971  fourierdlem12  47073  fourierdlem20  47081  fourierdlem25  47086  fourierdlem37  47098  fourierdlem41  47102  fourierdlem48  47108  fourierdlem50  47110  fourierdlem54  47114  fourierdlem64  47124  fourierdlem73  47133  fourierdlem79  47139  fourierdlem102  47162  fourierdlem111  47171  fourierdlem114  47174  etransclem23  47211  etransclem48  47236  ormkglobd  47831  chnsubseq  47834  2elfz2melfz  48332  elfzlble  48334  ceilhalfelfzo1  48348  1elfzo1ceilhalf1  48355  difltmodne  48362  modm2nep1  48386  modm1nep2  48388  modm1p1ne  48390  iccpartiltu  48448  iccpartigtl  48449  iccpartlt  48450  iccpartgt  48453  lswn0  48470  fmtnoge3  48559  fmtnodvds  48573  odz2prm2pw  48592  fmtnole4prm  48607  lighneallem4b  48638  nprmdvdsfacm1lem3  48651  nprmdvdsfacm1lem4  48652  nprmdvdsfacm1  48653  mogoldbb  48827  nnsum4primesevenALTV  48843  bgoldbtbndlem3  48849  gpgprismgriedgdmss  49094  gpgprismgrusgra  49100  gpg3nbgrvtx0  49118  gpg3nbgrvtx0ALT  49119  gpg5nbgrvtx03star  49122  gpg5nbgr3star  49123  gpg3kgrtriexlem3  49127  gpg3kgrtriexlem4  49128  gpg3kgrtriexlem6  49130  gpgprismgr4cycllem3  49139  gpgprismgr4cycllem9  49145  ssnn0ssfz  49405  lmod1  49548  elfzolborelfzop1  49575  nnolog2flm1  49646  funcf2lem2  50134  isnatd  50275