Theorem syl3anbrc 1350

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  soisores  7278  limuni3  7799  onfununi  8278  smores2  8291  smoiso  8299  oelimcl  8533  iserd  8667  resixp  8878  undifixp  8879  alephval3  10030  canthwelem  10571  canthwe  10572  r1limwun  10657  wunex2  10659  tskcard  10702  gruina  10739  eluzmn  12793  eluzuzle  12795  uztrn  12804  eluzadd  12815  eluzsub  12816  subeluzsub  12819  nn0pzuz  12853  zsupss  12885  nn0ge2m1nnALT  12890  xov1plusxeqvd  13449  ige2m1fz  13569  0elfz  13576  uzsubfz0  13588  elfzmlbm  13590  difelfzle  13593  difelfznle  13594  fvffz0  13598  elfzod  13615  elfzolt2b  13623  elfzolt3b  13624  elfzouz2  13627  fzossrbm1  13641  elfzo0  13653  eluzgtdifelfzo  13680  elfzodifsumelfzo  13684  fzonn0p1  13695  fzonn0p1p1  13697  fzo0sn0fzo1  13708  ssfzo12bi  13714  fzoopth  13715  ubmelm1fzo  13716  elfzonelfzo  13722  fzosplitprm1  13731  fzostep1  13739  fvinim0ffz  13742  flword2  13770  uzsup  13820  modfzo0difsn  13903  modsumfzodifsn  13904  fsuppmapnn0fiub  13951  suppssfz  13954  1elfz0hash  14350  fzsdom2  14388  ccatdmss  14542  ccatrn  14550  ccat2s1fvw  14599  pfxn0  14647  pfxtrcfv0  14654  pfxtrcfvl  14657  swrdswrd  14665  swrdccatin1  14685  pfxccat3  14694  pfxccat3a  14698  repswswrd  14744  cshwidxmod  14763  cshw1  14782  cshwcsh2id  14788  swrds2  14900  pfx2  14907  2swrd2eqwrdeq  14913  ccat2s1fvwALT  14915  rexuzre  15313  limsupgre  15441  rlimclim1  15505  rlimclim  15506  climrlim2  15507  isercolllem1  15625  isercoll  15628  climcndslem1  15812  fallfacval4  16006  tanhbnd  16126  sinbnd2  16147  cosbnd2  16148  rpnnen2lem12  16190  nn0o  16350  bitsfzolem  16401  bitsfzo  16402  bitsmod  16403  bitsfi  16404  bitsinv1lem  16408  bitsinv1  16409  smueqlem  16457  dvdsnprmd  16657  2mulprm  16660  hashgcdlem  16756  prm23lt5  16783  zgz  16902  gznegcl  16904  gzcjcl  16905  gzaddcl  16906  gzmulcl  16907  vdwlem9  16958  prmgaplem3  17022  prmgaplem4  17023  cshwshashlem2  17065  setsstruct2  17142  ismred  17562  isfuncd  17830  homdmcoa  18032  isdrs2  18270  fpwipodrs  18504  ipodrsima  18505  chnub  18586  chnso  18588  sgrp2rid2ex  18896  subgid  19102  issubg2  19115  subsubg  19123  gaorber  19281  orbsta  19286  pmtrfconj  19439  psgnunilem2  19468  psgnunilem3  19469  psgnunilem4  19470  pgpfi1  19568  subgpgp  19570  pgpssslw  19587  subgslw  19589  sylow2alem2  19591  fislw  19598  sylow3lem3  19602  efgs1  19708  efgsp1  19710  efgsres  19711  efgredleme  19716  efgcpbllemb  19728  lt6abl  19868  telgsumfzs  19962  ablfac1eu  20048  submomnd  20105  isrngd  20152  prdsrngd  20155  ringrng  20264  isringrng  20266  isringd  20270  ringsrg  20276  ring1  20289  prdsringd  20298  subrngid  20528  subrngsubg  20531  issubrng2  20537  subsubrng  20542  subrgsubg  20556  subrgsubrng  20557  sdrgid  20771  cntzsdrg  20781  subdrgint  20782  sdrgint  20783  suborng  20855  islmodd  20863  islssd  20932  islss4  20959  dflidl2rng  21218  rnglidl0  21229  rnglidl1  21232  rnglidlrng  21247  rng2idlsubrng  21265  rhmpreimaidl  21277  gzrngunit  21415  expmhm  21418  zringunit  21448  prmirredlem  21454  znidomb  21543  isphld  21636  ocvocv  21653  ocvlss  21654  frlmlbs  21779  psdmul  22161  gsummoncoe1  22301  mp2pm2mplem4  22799  chfacfisf  22844  chfacfisfcpmat  22845  chfacfscmulfsupp  22849  chfacfpmmulfsupp  22853  chfacfpmmulgsum2  22855  2ndcctbss  23445  finlocfin  23510  dissnlocfin  23519  locfindis  23520  locfincf  23521  isfild  23848  infil  23853  neifil  23870  flimfcls  24016  istgp2  24081  oppgtmd  24087  oppgtgp  24088  distgp  24089  indistgp  24090  efmndtmd  24091  submtmd  24094  subgtgp  24095  symgtgp  24096  qustgplem  24111  prdstmdd  24114  prdstgpd  24115  tlmtgp  24186  isngp4  24602  subgngp  24625  ngptgp  24626  tngngp2  24642  nrgtrg  24680  nrgtdrg  24683  elii2  24928  icopnfcnv  24934  xrhmeo  24938  lebnumii  24958  phtpcer  24987  reparpht  24990  phtpcco2  24991  pcohtpy  25012  pcoass  25016  pcorevlem  25018  isclmi  25069  isncvsngpd  25142  cphsubrglem  25169  cphclm  25181  phclm  25224  tcphcph  25229  clsocv  25242  cphsscph  25243  cmslssbn  25364  pjthlem2  25430  ovolf  25474  iundisj2  25541  vitalilem2  25601  vitali  25605  itg2monolem3  25744  dvfsumlem1  26018  dvfsumlem3  26020  mon1puc1p  26141  uc1pmon1p  26142  mon1pid  26144  ply1remlem  26155  drnguc1p  26164  plyaddlem1  26203  coeidlem  26227  aannenlem2  26320  radcnvcl  26407  pilem2  26442  coseq00topi  26491  coseq0negpitopi  26492  tangtx  26494  tanabsge  26495  cosq14gt0  26499  cosq14ge0  26500  cosq34lt1  26516  cosordlem  26519  cos0pilt1  26521  sinord  26523  resinf1o  26525  tanord1  26526  tanord  26527  efif1olem3  26533  efsubm  26540  relogrn  26550  logimclad  26561  logrnaddcl  26563  logneg  26577  logcj  26595  argregt0  26599  argrege0  26600  argimgt0  26601  argimlt0  26602  logimul  26603  logneg2  26604  logdmnrp  26630  logcnlem4  26634  dvloglem  26637  logf1o2  26639  efopnlem2  26646  cxpsqrtlem  26691  relogbval  26761  nnlogbexp  26770  relogbcxp  26774  relogbcxpb  26776  logbgt0b  26782  asinneg  26875  asinsin  26881  acoscos  26882  acosbnd  26889  atancj  26899  atanlogaddlem  26902  atanlogsublem  26904  atanlogsub  26905  atantan  26912  atanbndlem  26914  atans2  26920  leibpi  26931  scvxcvx  26974  jensenlem2  26976  emcllem7  26990  basellem1  27069  ppisval  27092  chtdif  27146  ppidif  27151  ppiub  27192  chtublem  27199  chtub  27200  lgsdilem2  27321  gausslemma2dlem1a  27353  gausslemma2dlem2  27355  gausslemma2dlem5  27359  gausslemma2dlem6  27360  lgsquadlem1  27368  lgsquadlem2  27369  lgsquadlem3  27370  2lgslem1  27382  2sqlem3  27408  chebbnd1lem1  27457  chebbnd1lem2  27458  chebbnd1lem3  27459  dchrisumlem2  27478  dchrvmasumlem2  27486  dchrvmasumiflem1  27489  dchrisum0flblem2  27497  mulog2sumlem2  27523  logdivbnd  27544  pntpbnd2  27575  pntibndlem1  27577  pntibnd  27581  pntlemc  27583  pntlemg  27586  pntlemq  27589  pntlemf  27593  padicabvf  27619  padicabvcxp  27620  ostth2  27625  noextend  27655  noextendseq  27656  nosupno  27692  noinfno  27707  ttgcontlem1  28978  axpaschlem  29034  nbgr2vtx1edg  29444  nbuhgr2vtx1edgb  29446  cusgrexi  29537  structtocusgr  29540  pthdadjvtx  29821  pthdlem1  29859  pthd  29862  crctcshwlkn0lem3  29905  crctcshwlkn0lem4  29906  crctcshwlkn0lem5  29907  crctcshwlkn0lem7  29909  wlkiswwlks1  29960  wwlksm1edg  29974  wwlksnred  29985  wwlksnredwwlkn  29988  wwlksnextproplem3  30004  clwlkclwwlklem2fv1  30090  clwlkclwwlklem2fv2  30091  clwlkclwwlklem2a  30093  clwlkclwwlklem2  30095  clwwisshclwwslemlem  30108  clwwisshclwwslem  30109  erclwwlkref  30115  clwwlkel  30141  clwwlkf  30142  wwlksext2clwwlk  30152  wwlksubclwwlk  30153  umgr2cwwkdifex  30160  1pthd  30238  eucrctshift  30338  dlwwlknondlwlknonf1olem1  30459  numclwlk2lem2f  30472  frgrreggt1  30488  grpoinvf  30628  strlem3a  32348  hstrlem3a  32356  iundisj2f  32686  fcoinver  32700  fresf1o  32730  ssnnssfz  32886  bcm1n  32894  iundisj2fi  32896  fsumrp0cl  33107  cycpmco2lem6  33219  fxpsdrg  33263  lmodslmd  33292  fldgensdrg  33405  intlidl  33510  idlinsubrg  33521  rhmimaidl  33522  ssdifidllem  33546  ssmxidllem  33563  1arithidomlem1  33625  1arithidomlem2  33626  1arithidom  33627  fldextsdrg  33845  fldextrspunlem2  33868  fldextrspundgdvdslem  33871  fldextrspundgdvds  33872  minplyirred  33902  algextdeglem4  33911  algextdeglem8  33915  rtelextdg2lem  33917  constrsdrg  33966  2sqr3minply  33971  cos9thpiminply  33979  locfinreflem  34031  locfinref  34032  xrge0iifcnv  34124  xrge0iifiso  34126  xrge0iifhom  34128  esumc  34242  esumle  34249  esumlef  34253  esumpinfsum  34268  esumpcvgval  34269  fiunelros  34365  voliune  34420  volfiniune  34421  sibfinima  34530  eulerpartlemt  34562  fiblem  34589  fibp1  34592  dstrvprob  34663  ballotlemsel1i  34704  ballotlemfrceq  34720  plymulx0  34738  signstfvc  34765  signstfveq0  34768  bnj944  35127  bnj998  35146  bnj1136  35186  bnj1408  35225  erdszelem4  35429  erdszelem8  35433  txsconnlem  35475  cvxsconn  35478  cvmliftpht  35553  snmlff  35564  elmrsubrn  35755  msrf  35777  mthmpps  35817  sinccvglem  35907  trer  36551  poimirlem6  38000  poimirlem7  38001  poimirlem9  38003  poimirlem17  38011  poimirlem20  38014  poimirlem28  38022  poimirlem29  38023  poimirlem30  38024  poimirlem31  38025  poimirlem32  38026  areacirc  38087  nnubfi  38124  prter1  39378  lkrlss  39594  diaf11N  41548  dibf11N  41660  lclkr  42032  lclkrs  42038  lcfrlem9  42049  lcfr  42084  mapd1o  42147  hdmapf1oN  42364  hgmapf1oN  42402  frlmvscadiccat  43003  fimgmcyc  43027  nacsfix  43168  eldioph2lem1  43216  irrapxlem1  43274  rmxypairf1o  43363  jm2.27a  43457  hbtlem2  43576  hbt  43582  mon1psubm  43651  onnoxpg  43880  pren2d  44007  binomcxplemnotnn0  44807  elixpconstg  45543  elfzfzo  45732  monoords  45752  eluzd  45859  fmul01lt1lem2  46037  sumnnodd  46082  ioodvbdlimc1lem2  46382  ioodvbdlimc2lem  46384  iblsplit  46416  iblspltprt  46423  itgspltprt  46429  stoweidlem11  46461  stoweidlem17  46467  fourierdlem12  46569  fourierdlem20  46577  fourierdlem25  46582  fourierdlem37  46594  fourierdlem41  46598  fourierdlem48  46604  fourierdlem49  46605  fourierdlem50  46606  fourierdlem54  46610  fourierdlem64  46620  fourierdlem73  46629  fourierdlem79  46635  fourierdlem102  46658  fourierdlem111  46667  fourierdlem114  46670  etransclem23  46707  etransclem48  46732  ormkglobd  47327  chnsubseq  47332  2elfz2melfz  47788  elfzlble  47790  ceilhalfelfzo1  47804  1elfzo1ceilhalf1  47811  difltmodne  47818  modm2nep1  47842  modm1nep2  47844  modm1p1ne  47846  iccpartiltu  47904  iccpartigtl  47905  iccpartlt  47906  iccpartgt  47909  lswn0  47926  fmtnoge3  48015  fmtnodvds  48029  odz2prm2pw  48048  fmtnole4prm  48063  lighneallem4b  48094  nprmdvdsfacm1lem3  48107  nprmdvdsfacm1lem4  48108  nprmdvdsfacm1  48109  mogoldbb  48283  nnsum4primesevenALTV  48299  bgoldbtbndlem3  48305  gpgprismgriedgdmss  48550  gpgprismgrusgra  48556  gpg3nbgrvtx0  48574  gpg3nbgrvtx0ALT  48575  gpg5nbgrvtx03star  48578  gpg5nbgr3star  48579  gpg3kgrtriexlem3  48583  gpg3kgrtriexlem4  48584  gpg3kgrtriexlem6  48586  gpgprismgr4cycllem3  48595  gpgprismgr4cycllem9  48601  ssnn0ssfz  48847  lmod1  48990  elfzolborelfzop1  49017  nnolog2flm1  49088  funcf2lem2  49579  isnatd  49720