Theorem syl3anbrc 1343

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 233	1 ⊢ (𝜑 → 𝜏)

Syntax hints:   → wi 4   ↔ wb 205   ∧ w3a 1087

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 206  df-an 397  df-3an 1089

This theorem is referenced by:  soisores  7326  limuni3  7843  onfununi  8343  smores2  8356  smoiso  8364  oelimcl  8602  iserd  8731  resixp  8929  undifixp  8930  alephval3  10107  canthwelem  10647  canthwe  10648  r1limwun  10733  wunex2  10735  tskcard  10778  gruina  10815  eluzmn  12831  eluzuzle  12833  uztrn  12842  eluzadd  12853  eluzsub  12854  subeluzsub  12861  nn0pzuz  12891  zsupss  12923  nn0ge2m1nnALT  12928  xov1plusxeqvd  13477  ige2m1fz  13593  0elfz  13600  uzsubfz0  13611  elfzmlbm  13613  difelfzle  13616  difelfznle  13617  fvffz0  13621  elfzolt2b  13645  elfzolt3b  13646  elfzouz2  13649  fzossrbm1  13663  elfzo0  13675  eluzgtdifelfzo  13696  elfzodifsumelfzo  13700  fzonn0p1  13711  fzonn0p1p1  13713  fzo0sn0fzo1  13723  ssfzo12bi  13729  ubmelm1fzo  13730  elfzonelfzo  13736  fzosplitprm1  13744  fzostep1  13750  fvinim0ffz  13753  flword2  13780  uzsup  13830  modfzo0difsn  13910  modsumfzodifsn  13911  fsuppmapnn0fiub  13958  suppssfz  13961  1elfz0hash  14352  fzsdom2  14390  ccatrn  14541  ccat2s1fvw  14590  pfxn0  14638  pfxtrcfv0  14646  pfxtrcfvl  14649  swrdswrd  14657  swrdccatin1  14677  pfxccat3  14686  pfxccat3a  14690  repswswrd  14736  cshwidxmod  14755  cshw1  14774  cshwcsh2id  14781  swrds2  14893  pfx2  14900  2swrd2eqwrdeq  14906  ccat2s1fvwALT  14908  rexuzre  15301  limsupgre  15427  rlimclim1  15491  rlimclim  15492  climrlim2  15493  isercolllem1  15613  isercoll  15616  climcndslem1  15797  fallfacval4  15989  tanhbnd  16106  sinbnd2  16127  cosbnd2  16128  rpnnen2lem12  16170  nn0o  16328  bitsfzolem  16377  bitsfzo  16378  bitsmod  16379  bitsfi  16380  bitsinv1lem  16384  bitsinv1  16385  smueqlem  16433  dvdsnprmd  16629  2mulprm  16632  hashgcdlem  16723  prm23lt5  16749  zgz  16868  gznegcl  16870  gzcjcl  16871  gzaddcl  16872  gzmulcl  16873  vdwlem9  16924  prmgaplem3  16988  prmgaplem4  16989  cshwshashlem2  17032  setsstruct2  17109  ismred  17548  isfuncd  17817  homdmcoa  18019  isdrs2  18261  fpwipodrs  18495  ipodrsima  18496  sgrp2rid2ex  18810  subgid  19010  issubg2  19023  subsubg  19031  gaorber  19174  orbsta  19179  pmtrfconj  19336  psgnunilem2  19365  psgnunilem3  19366  psgnunilem4  19367  pgpfi1  19465  subgpgp  19467  pgpssslw  19484  subgslw  19486  sylow2alem2  19488  fislw  19495  sylow3lem3  19499  efgs1  19605  efgsp1  19607  efgsres  19608  efgredleme  19613  efgcpbllemb  19625  lt6abl  19765  telgsumfzs  19859  ablfac1eu  19945  isringd  20107  ringsrg  20113  ring1  20126  prdsringd  20138  subrgsubg  20329  sdrgid  20412  cntzsdrg  20422  subdrgint  20423  sdrgint  20424  islmodd  20481  islssd  20551  islss4  20578  dflidl2lem  20848  gzrngunit  21017  expmhm  21020  zringunit  21042  prmirredlem  21048  znidomb  21123  isphld  21213  ocvocv  21230  ocvlss  21231  frlmlbs  21358  gsummoncoe1  21835  mp2pm2mplem4  22318  chfacfisf  22363  chfacfisfcpmat  22364  chfacfscmulfsupp  22368  chfacfpmmulfsupp  22372  chfacfpmmulgsum2  22374  2ndcctbss  22966  finlocfin  23031  dissnlocfin  23040  locfindis  23041  locfincf  23042  isfild  23369  infil  23374  neifil  23391  flimfcls  23537  istgp2  23602  oppgtmd  23608  oppgtgp  23609  distgp  23610  indistgp  23611  efmndtmd  23612  submtmd  23615  subgtgp  23616  symgtgp  23617  qustgplem  23632  prdstmdd  23635  prdstgpd  23636  tlmtgp  23707  isngp4  24128  subgngp  24151  ngptgp  24152  tngngp2  24176  nrgtrg  24214  nrgtdrg  24217  elii2  24459  icopnfcnv  24465  xrhmeo  24469  lebnumii  24489  phtpcer  24518  reparpht  24521  phtpcco2  24522  pcohtpy  24543  pcoass  24547  pcorevlem  24549  isclmi  24600  isncvsngpd  24674  cphsubrglem  24701  cphclm  24713  phclm  24756  tcphcph  24761  clsocv  24774  cphsscph  24775  cmslssbn  24896  pjthlem2  24962  ovolf  25006  iundisj2  25073  vitalilem2  25133  vitali  25137  itg2monolem3  25277  dvfsumlem1  25550  dvfsumlem3  25552  mon1puc1p  25675  uc1pmon1p  25676  ply1remlem  25687  drnguc1p  25695  plyaddlem1  25734  coeidlem  25758  aannenlem2  25849  radcnvcl  25936  pilem2  25971  coseq00topi  26019  coseq0negpitopi  26020  tangtx  26022  tanabsge  26023  cosq14gt0  26027  cosq14ge0  26028  cosq34lt1  26043  cosordlem  26046  cos0pilt1  26048  sinord  26050  resinf1o  26052  tanord1  26053  tanord  26054  efif1olem3  26060  efsubm  26067  relogrn  26077  logimclad  26088  logrnaddcl  26090  logneg  26103  logcj  26121  argregt0  26125  argrege0  26126  argimgt0  26127  argimlt0  26128  logimul  26129  logneg2  26130  logdmnrp  26156  logcnlem4  26160  dvloglem  26163  logf1o2  26165  efopnlem2  26172  cxpsqrtlem  26217  relogbval  26284  nnlogbexp  26293  relogbcxp  26297  relogbcxpb  26299  logbgt0b  26305  asinneg  26398  asinsin  26404  acoscos  26405  acosbnd  26412  atancj  26422  atanlogaddlem  26425  atanlogsublem  26427  atanlogsub  26428  atantan  26435  atanbndlem  26437  atans2  26443  leibpi  26454  scvxcvx  26497  jensenlem2  26499  emcllem7  26513  basellem1  26592  ppisval  26615  chtdif  26669  ppidif  26674  ppiub  26714  chtublem  26721  chtub  26722  lgsdilem2  26843  gausslemma2dlem1a  26875  gausslemma2dlem2  26877  gausslemma2dlem5  26881  gausslemma2dlem6  26882  lgsquadlem1  26890  lgsquadlem2  26891  lgsquadlem3  26892  2lgslem1  26904  2sqlem3  26930  chebbnd1lem1  26979  chebbnd1lem2  26980  chebbnd1lem3  26981  dchrisumlem2  27000  dchrvmasumlem2  27008  dchrvmasumiflem1  27011  dchrisum0flblem2  27019  mulog2sumlem2  27045  logdivbnd  27066  pntpbnd2  27097  pntibndlem1  27099  pntibnd  27103  pntlemc  27105  pntlemg  27108  pntlemq  27111  pntlemf  27115  padicabvf  27141  padicabvcxp  27142  ostth2  27147  noextend  27176  noextendseq  27177  nosupno  27213  noinfno  27228  ttgcontlem1  28180  axpaschlem  28236  nbgr2vtx1edg  28645  nbuhgr2vtx1edgb  28647  cusgrexi  28738  structtocusgr  28741  pthdadjvtx  29025  pthdlem1  29061  pthd  29064  crctcshwlkn0lem3  29104  crctcshwlkn0lem4  29105  crctcshwlkn0lem5  29106  crctcshwlkn0lem7  29108  wlkiswwlks1  29159  wwlksm1edg  29173  wwlksnred  29184  wwlksnredwwlkn  29187  wwlksnextproplem3  29203  clwlkclwwlklem2fv1  29286  clwlkclwwlklem2fv2  29287  clwlkclwwlklem2a  29289  clwlkclwwlklem2  29291  clwwisshclwwslemlem  29304  clwwisshclwwslem  29305  erclwwlkref  29311  clwwlkel  29337  clwwlkf  29338  wwlksext2clwwlk  29348  wwlksubclwwlk  29349  umgr2cwwkdifex  29356  1pthd  29434  eucrctshift  29534  dlwwlknondlwlknonf1olem1  29655  numclwlk2lem2f  29668  frgrreggt1  29684  grpoinvf  29823  strlem3a  31543  hstrlem3a  31551  iundisj2f  31859  fcoinver  31873  fresf1o  31893  ssnnssfz  32036  bcm1n  32044  iundisj2fi  32046  fsumrp0cl  32234  submomnd  32269  cycpmco2lem6  32331  lmodslmd  32390  fldgensdrg  32445  suborng  32474  intlidl  32581  rhmpreimaidl  32582  idlinsubrg  32594  rhmimaidl  32595  ssmxidllem  32634  minplyirred  32830  algextdeglem4  32836  algextdeglem8  32840  locfinreflem  32889  locfinref  32890  xrge0iifcnv  32982  xrge0iifiso  32984  xrge0iifhom  32986  esumc  33118  esumle  33125  esumlef  33129  esumpinfsum  33144  esumpcvgval  33145  fiunelros  33241  voliune  33296  volfiniune  33297  sibfinima  33407  eulerpartlemt  33439  fiblem  33466  fibp1  33469  dstrvprob  33539  ballotlemsel1i  33580  ballotlemfrceq  33596  plymulx0  33627  signstfvc  33654  signstfveq0  33657  bnj944  34018  bnj998  34037  bnj1136  34077  bnj1408  34116  erdszelem4  34254  erdszelem8  34258  txsconnlem  34300  cvxsconn  34303  cvmliftpht  34378  snmlff  34389  elmrsubrn  34580  msrf  34602  mthmpps  34642  sinccvglem  34726  trer  35287  poimirlem6  36580  poimirlem7  36581  poimirlem9  36583  poimirlem17  36591  poimirlem20  36594  poimirlem28  36602  poimirlem29  36603  poimirlem30  36604  poimirlem31  36605  poimirlem32  36606  areacirc  36667  nnubfi  36704  prter1  37835  lkrlss  38051  diaf11N  40006  dibf11N  40118  lclkr  40490  lclkrs  40496  lcfrlem9  40507  lcfr  40542  mapd1o  40605  hdmapf1oN  40822  hgmapf1oN  40860  frlmvscadiccat  41166  sn-inelr  41420  nacsfix  41532  eldioph2lem1  41580  irrapxlem1  41642  rmxypairf1o  41732  jm2.27a  41826  hbtlem2  41948  hbt  41954  mon1pid  42029  mon1psubm  42030  onnog  42262  pren2d  42389  binomcxplemnotnn0  43197  elixpconstg  43860  elfzfzo  44065  monoords  44086  elfzod  44189  eluzd  44198  fmul01lt1lem2  44380  sumnnodd  44425  ioodvbdlimc1lem2  44727  ioodvbdlimc2lem  44729  iblsplit  44761  iblspltprt  44768  itgspltprt  44774  stoweidlem11  44806  stoweidlem17  44812  fourierdlem12  44914  fourierdlem20  44922  fourierdlem25  44927  fourierdlem37  44939  fourierdlem41  44943  fourierdlem48  44949  fourierdlem49  44950  fourierdlem50  44951  fourierdlem54  44955  fourierdlem64  44965  fourierdlem73  44974  fourierdlem79  44980  fourierdlem102  45003  fourierdlem111  45012  fourierdlem114  45015  etransclem23  45052  etransclem48  45077  2elfz2melfz  46105  elfzlble  46107  fzoopth  46114  iccpartiltu  46169  iccpartigtl  46170  iccpartlt  46171  iccpartgt  46174  lswn0  46191  fmtnoge3  46277  fmtnodvds  46291  odz2prm2pw  46310  fmtnole4prm  46325  lighneallem4b  46356  mogoldbb  46532  nnsum4primesevenALTV  46548  bgoldbtbndlem3  46554  ringrng  46734  isringrng  46736  isrngd  46751  prdsrngd  46756  subrngid  46807  subrngsubg  46810  issubrng2  46816  subsubrng  46821  dflidl2rng  46829  rnglidl0  46831  rnglidl1  46832  rnglidlrng  46837  rng2idlsubrng  46839  ssnn0ssfz  47104  lmod1  47251  elfzolborelfzop1  47278  nnolog2flm1  47354