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  7335  mpt3fvotd  7689  limuni3  7863  onfununi  8349  smores2  8362  smoiso  8370  oelimcl  8609  iserd  8744  resixp  8961  undifixp  8962  alephval3  10189  canthwelem  10735  canthwe  10736  r1limwun  10821  wunex2  10823  tskcard  10866  gruina  10903  eluzmn  12972  eluzuzle  12974  uztrn  12983  eluzadd  12994  eluzsub  12995  subeluzsub  12998  nn0pzuz  13032  zsupss  13064  nn0ge2m1nnALT  13069  xov1plusxeqvd  13629  ige2m1fz  13751  0elfz  13758  uzsubfz0  13770  elfzmlbm  13772  difelfzle  13775  difelfznle  13776  fvffz0  13780  elfzod  13797  elfzolt2b  13805  elfzolt3b  13806  elfzouz2  13809  fzossrbm1  13823  elfzo0  13835  eluzgtdifelfzo  13862  elfzodifsumelfzo  13866  fzonn0p1  13877  fzonn0p1p1  13879  fzo0sn0fzo1  13890  ssfzo12bi  13896  fzoopth  13897  ubmelm1fzo  13898  elfzonelfzo  13904  fzosplitprm1  13913  fzostep1  13921  fvinim0ffz  13924  flword2  13953  uzsup  14003  modfzo0difsn  14086  modsumfzodifsn  14087  fsuppmapnn0fiub  14134  suppssfz  14137  1elfz0hash  14534  fzsdom2  14573  ccatdmss  14727  ccatrn  14735  ccat2s1fvw  14786  pfxn0  14836  pfxtrcfv0  14843  pfxtrcfvl  14846  swrdswrd  14854  swrdccatin1  14874  pfxccat3  14883  pfxccat3a  14887  repswswrd  14935  cshwidxmod  14954  cshw1  14973  cshwcsh2id  14979  swrds2  15091  pfx2  15098  2swrd2eqwrdeq  15106  ccat2s1fvwALT  15108  rexuzre  15520  limsupgre  15648  rlimclim1  15712  rlimclim  15713  climrlim2  15714  isercolllem1  15832  isercoll  15835  climcndslem1  16018  fallfacval4  16209  tanhbnd  16329  sinbnd2  16350  cosbnd2  16351  rpnnen2lem12  16393  nn0o  16553  bitsfzolem  16604  bitsfzo  16605  bitsmod  16606  bitsfi  16607  bitsinv1lem  16611  bitsinv1  16612  smueqlem  16660  dvdsnprmd  16865  2mulprm  16868  hashgcdlem  16965  prm23lt5  16992  zgz  17111  gznegcl  17113  gzcjcl  17114  gzaddcl  17115  gzmulcl  17116  vdwlem9  17167  prmgaplem3  17231  prmgaplem4  17232  cshwshashlem2  17274  setsstruct2  17352  ismred  17772  isfuncd  18040  homdmcoa  18242  isdrs2  18480  fpwipodrs  18714  ipodrsima  18715  chnub  18796  chnso  18798  sgrp2rid2ex  19126  subgid  19338  issubg2  19352  subsubg  19360  gaorber  19522  orbsta  19527  pmtrfconj  19680  psgnunilem2  19709  psgnunilem3  19710  psgnunilem4  19711  pgpfi1  19809  subgpgp  19811  pgpssslw  19828  subgslw  19830  sylow2alem2  19832  fislw  19839  sylow3lem3  19843  efgs1  19949  efgsp1  19951  efgsres  19952  efgredleme  19957  efgcpbllemb  19969  lt6abl  20109  telgsumfzs  20203  ablfac1eu  20289  submomnd  20346  isrngd  20395  prdsrngd  20398  ringrng  20514  isringrng  20516  isringd  20522  ringsrg  20528  ring1  20541  prdsringd  20550  subrngid  20801  subrngsubg  20804  issubrng2  20810  subsubrng  20815  subrgsubg  20829  subrgsubrng  20830  sdrgid  21049  cntzsdrg  21059  subdrgint  21060  sdrgint  21061  suborng  21133  islmodd  21141  islssd  21210  islss4  21237  dflidl2rng  21497  rnglidl0  21509  rnglidl1  21512  unichnlidl  21516  rnglidlrng  21535  rng2idlsubrng  21559  rhmpreimaidl  21571  ssdifidllem  21640  gzrngunit  21739  expmhm  21742  zringunit  21772  prmirredlem  21778  znidomb  21867  isphld  21960  ocvocv  21977  ocvlss  21978  frlmlbs  22103  psdmul  22487  gsummoncoe1  22626  mp2pm2mplem4  23127  chfacfisf  23172  chfacfisfcpmat  23173  chfacfscmulfsupp  23177  chfacfpmmulfsupp  23181  chfacfpmmulgsum2  23183  2ndcctbss  23774  finlocfin  23839  dissnlocfin  23848  locfindis  23849  locfincf  23850  isfild  24177  infil  24182  neifil  24199  flimfcls  24345  istgp2  24410  oppgtmd  24416  oppgtgp  24417  distgp  24418  indistgp  24419  efmndtmd  24420  submtmd  24423  subgtgp  24424  symgtgp  24425  qustgplem  24440  prdstmdd  24443  prdstgpd  24444  tlmtgp  24515  isngp4  24931  subgngp  24954  ngptgp  24955  tngngp2  24971  nrgtrg  25009  nrgtdrg  25012  elii2  25257  icopnfcnv  25263  xrhmeo  25267  lebnumii  25287  phtpcer  25316  reparpht  25319  phtpcco2  25320  pcohtpy  25341  pcoass  25345  pcorevlem  25347  isclmi  25398  isncvsngpd  25471  cphsubrglem  25498  cphclm  25510  phclm  25553  tcphcph  25558  clsocv  25571  cphsscph  25572  cmslssbn  25693  pjthlem2  25759  ovolf  25803  iundisj2  25870  vitalilem2  25930  vitali  25934  itg2monolem3  26073  dvfsumlem1  26346  dvfsumlem3  26348  mon1puc1p  26469  uc1pmon1p  26470  mon1pid  26472  ply1remlem  26483  drnguc1p  26492  plyaddlem1  26532  coeidlem  26556  plyn0mulidp  26602  aannenlem2  26656  radcnvcl  26744  pilem2  26779  coseq00topi  26831  coseq0negpitopi  26832  tangtx  26834  tanabsge  26835  cosq14gt0  26839  cosq14ge0  26840  cosq34lt1  26855  cosordlem  26858  cos0pilt1  26860  sinord  26862  resinf1o  26864  tanord1  26865  tanord  26866  efif1olem3  26872  efsubm  26879  relogrn  26889  logimclad  26900  logrnaddcl  26902  logneg  26916  logcj  26934  argregt0  26938  argrege0  26939  argimgt0  26940  argimlt0  26941  logimul  26942  logneg2  26943  logdmnrp  26969  logcnlem4  26973  dvloglem  26976  logf1o2  26978  efopnlem2  26985  cxpsqrtlem  27030  relogbval  27100  nnlogbexp  27109  relogbcxp  27113  relogbcxpb  27115  logbgt0b  27121  asinneg  27214  asinsin  27220  acoscos  27221  acosbnd  27228  atancj  27238  atanlogaddlem  27241  atanlogsublem  27243  atanlogsub  27244  atantan  27251  atanbndlem  27253  atans2  27259  leibpi  27270  scvxcvx  27313  jensenlem2  27315  emcllem7  27329  basellem1  27408  ppisval  27431  chtdif  27485  ppidif  27490  ppiub  27531  chtublem  27538  chtub  27539  lgsdilem2  27660  gausslemma2dlem1a  27692  gausslemma2dlem2  27694  gausslemma2dlem5  27698  gausslemma2dlem6  27699  lgsquadlem1  27707  lgsquadlem2  27708  lgsquadlem3  27709  2lgslem1  27721  2sqlem3  27747  chebbnd1lem1  27796  chebbnd1lem2  27797  chebbnd1lem3  27798  dchrisumlem2  27817  dchrvmasumlem2  27825  dchrvmasumiflem1  27828  dchrisum0flblem2  27836  mulog2sumlem2  27862  logdivbnd  27883  pntpbnd2  27914  pntibndlem1  27916  pntibnd  27920  pntlemc  27922  pntlemg  27925  pntlemq  27928  pntlemf  27932  padicabvf  27958  padicabvcxp  27959  ostth2  27964  fltoprmlem2  27994  noextend  28023  noextendseq  28024  nosupno  28060  noinfno  28075  ttgcontlem1  29462  axpaschlem  29518  nbgr2vtx1edg  29931  nbuhgr2vtx1edgb  29933  cusgrexi  30024  structtocusgr  30027  pthdadjvtx  30313  pthdlem1  30352  pthd  30355  crctcshwlkn0lem3  30401  crctcshwlkn0lem4  30402  crctcshwlkn0lem5  30403  crctcshwlkn0lem7  30405  wlkiswwlks1  30456  wwlksm1edg  30470  wwlksnred  30481  wwlksnredwwlkn  30484  wwlksnextproplem3  30500  clwlkclwwlklem2fv1  30586  clwlkclwwlklem2fv2  30587  clwlkclwwlklem2a  30589  clwlkclwwlklem2  30591  clwwisshclwwslemlem  30604  clwwisshclwwslem  30605  erclwwlkref  30611  clwwlkel  30637  clwwlkf  30638  wwlksext2clwwlk  30648  wwlksubclwwlk  30649  umgr2cwwkdifex  30656  1pthd  30734  eucrctshift  30844  dlwwlknondlwlknonf1olem1  30965  numclwlk2lem2f  30978  frgrreggt1  30994  grpoinvf  31134  strlem3a  32854  hstrlem3a  32862  iundisj2f  33184  fcoinver  33198  fresf1o  33225  ssnnssfz  33379  bcm1n  33387  iundisj2fi  33389  fsumrp0cl  33582  cycpmco2lem6  33692  fxpsdrg  33736  lmodslmd  33765  fldgensdrg  33876  intlidl  33970  idlinsubrg  33981  rhmimaidl  33982  ssmxidllem  33998  dflringlem2  34027  1arithidomlem1  34067  1arithidomlem2  34068  1arithidom  34069  fldextsdrg  34286  fldextrspunlem2  34309  fldextrspundgdvdslem  34312  fldextrspundgdvds  34313  minplyirred  34343  algextdeglem4  34352  algextdeglem8  34356  rtelextdg2lem  34358  constrsdrg  34407  2sqr3minply  34412  cos9thpiminply  34420  locfinreflem  34472  locfinref  34473  xrge0iifcnv  34565  xrge0iifiso  34567  xrge0iifhom  34569  esumc  34683  esumle  34690  esumlef  34694  esumpinfsum  34709  esumpcvgval  34710  fiunelros  34807  voliune  34862  volfiniune  34863  sibfinima  34971  eulerpartlemt  35003  fiblem  35030  fibp1  35033  dstrvprob  35104  ballotlemsel1i  35145  ballotlemfrceq  35161  signstfvc  35203  signstfveq0  35206  bnj944  35568  bnj998  35587  bnj1136  35627  bnj1408  35666  erdszelem4  35959  erdszelem8  35963  txsconnlem  36005  cvxsconn  36008  cvmliftpht  36083  snmlff  36094  elmrsubrn  36285  msrf  36307  mthmpps  36347  sinccvglem  36437  trer  37104  poimirlem6  38545  poimirlem7  38546  poimirlem9  38548  poimirlem17  38556  poimirlem20  38559  poimirlem28  38567  poimirlem29  38568  poimirlem30  38569  poimirlem31  38570  poimirlem32  38571  areacirc  38632  nnubfi  38685  prter1  39937  lkrlss  40153  diaf11N  42107  dibf11N  42219  lclkr  42591  lclkrs  42597  lcfrlem9  42608  lcfr  42643  mapd1o  42706  hdmapf1oN  42923  hgmapf1oN  42961  frlmvscadiccat  43574  fimgmcyc  43599  nacsfix  43723  eldioph2lem1  43771  irrapxlem1  43829  rmxypairf1o  43918  jm2.27a  44012  hbtlem2  44126  hbt  44132  mon1psubm  44201  onnoxpg  44430  pren2d  44557  binomcxplemnotnn0  45340  elixpconstg  46104  elfzfzo  46293  monoords  46313  eluzd  46419  fmul01lt1lem2  46597  sumnnodd  46642  ioodvbdlimc1lem2  46942  ioodvbdlimc2lem  46944  iblsplit  46976  iblspltprt  46983  itgspltprt  46989  stoweidlem11  47021  stoweidlem17  47027  fourierdlem12  47129  fourierdlem20  47137  fourierdlem25  47142  fourierdlem37  47154  fourierdlem41  47158  fourierdlem48  47164  fourierdlem50  47166  fourierdlem54  47170  fourierdlem64  47180  fourierdlem73  47189  fourierdlem79  47195  fourierdlem102  47218  fourierdlem111  47227  fourierdlem114  47230  etransclem23  47267  etransclem48  47292  ormkglobd  47887  chnsubseq  47890  2elfz2melfz  48388  elfzlble  48390  ceilhalfelfzo1  48404  1elfzo1ceilhalf1  48411  difltmodne  48418  modm2nep1  48442  modm1nep2  48444  modm1p1ne  48446  iccpartiltu  48504  iccpartigtl  48505  iccpartlt  48506  iccpartgt  48509  lswn0  48526  fmtnoge3  48615  fmtnodvds  48629  odz2prm2pw  48648  fmtnole4prm  48663  lighneallem4b  48694  nprmdvdsfacm1lem3  48707  nprmdvdsfacm1lem4  48708  nprmdvdsfacm1  48709  mogoldbb  48883  nnsum4primesevenALTV  48899  bgoldbtbndlem3  48905  gpgprismgriedgdmss  49150  gpgprismgrusgra  49156  gpg3nbgrvtx0  49174  gpg3nbgrvtx0ALT  49175  gpg5nbgrvtx03star  49178  gpg5nbgr3star  49179  gpg3kgrtriexlem3  49183  gpg3kgrtriexlem4  49184  gpg3kgrtriexlem6  49186  gpgprismgr4cycllem3  49195  gpgprismgr4cycllem9  49201  ssnn0ssfz  49461  lmod1  49604  elfzolborelfzop1  49631  nnolog2flm1  49702  funcf2lem2  50190  isnatd  50331