Theorem syl3anbrc 1239

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

Syntax hints:   → wi 4   ↔ wb 195   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  soisores  6477  limuni3  6944  onfununi  7325  smores2  7338  smoiso  7346  oelimcl  7567  iserd  7655  erinxp  7708  resixp  7829  undifixp  7830  alephval3  8816  fpwwe2lem12  9342  canthwelem  9351  canthwe  9352  r1limwun  9437  wunex2  9439  tskcard  9482  gruina  9519  nqerf  9631  nqerid  9634  eluzmn  11570  eluzuzle  11572  uztrn  11580  nn0pzuz  11621  zsupss  11653  nn0ge2m1nnALT  11658  xov1plusxeqvd  12189  ssfzunsn  12257  ige2m1fz  12299  0elfz  12305  uzsubfz0  12316  elfzmlbm  12318  difelfzle  12321  difelfznle  12322  fvffz0  12326  elfzolt2b  12350  elfzolt3b  12351  elfzouz2  12353  fzossrbm1  12366  elfzo0  12376  eluzgtdifelfzo  12397  elfzodifsumelfzo  12401  fzonn0p1  12411  fzonn0p1p1  12413  elfzom1p1elfzo  12414  fzo0sn0fzo1  12424  ssfzo12bi  12429  ubmelm1fzo  12430  elfzonelfzo  12436  fzosplitprm1  12443  fzostep1  12446  fvinim0ffz  12449  flword2  12476  uzsup  12524  modfzo0difsn  12604  modsumfzodifsn  12605  fsuppmapnn0fiub  12652  fsuppmapnn0fiubOLD  12653  suppssfz  12656  1elfz0hash  13040  fzsdom2  13075  ccatrn  13225  swrdn0  13282  swrdtrcfv  13293  swrdtrcfv0  13294  swrdeq  13296  swrdtrcfvl  13302  swrdswrd  13312  swrdccatwrd  13320  wrdeqs1cat  13326  swrdccatin1  13334  swrdccat3  13343  swrdccatid  13348  repswswrd  13382  cshwidxmod  13400  cshw1  13419  cshwcsh2id  13425  swrds2  13533  2swrd2eqwrdeq  13544  ccat2s1fvwALT  13546  rexuzre  13940  limsupgre  14060  rlimclim1  14124  rlimclim  14125  climrlim2  14126  isercolllem1  14243  isercoll  14246  climcndslem1  14420  fallfacval4  14613  tanhbnd  14730  sinbnd2  14751  cosbnd2  14752  rpnnen2lem12  14793  nn0o  14937  bitsfzolem  14994  bitsfzo  14995  bitsmod  14996  bitsfi  14997  bitsinv1lem  15001  bitsinv1  15002  smueqlem  15050  dvdsnprmd  15241  hashgcdlem  15331  prm23lt5  15357  zgz  15475  gznegcl  15477  gzcjcl  15478  gzaddcl  15479  gzmulcl  15480  vdwlem9  15531  prmgaplem3  15595  prmgaplem4  15596  cshwshashlem2  15641  ismred  16085  isfuncd  16348  homdmcoa  16540  isdrs2  16762  fpwipodrs  16987  ipodrsima  16988  psss  17037  psssdm2  17038  sgrp2rid2ex  17237  subgid  17419  issubg2  17432  subsubg  17440  gaorber  17564  orbsta  17569  pmtrfconj  17709  psgnunilem2  17738  psgnunilem3  17739  psgnunilem4  17740  pgpfi1  17833  subgpgp  17835  pgpssslw  17852  subgslw  17854  sylow2alem2  17856  fislw  17863  sylow3lem3  17867  efgs1  17971  efgsp1  17973  efgsres  17974  efgredleme  17979  efgcpbllemb  17991  lt6abl  18119  telgsumfzs  18209  ablfac1eu  18295  isringd  18408  ringsrg  18412  ring1  18425  prdsringd  18435  subrgsubg  18609  islmodd  18692  islssd  18757  islss4  18783  gsummoncoe1  19495  gzrngunit  19631  expmhm  19634  zringunit  19655  prmirredlem  19660  znidomb  19729  isphld  19818  ocvocv  19834  ocvlss  19835  frlmlbs  19955  mp2pm2mplem4  20433  chfacfisf  20478  chfacfisfcpmat  20479  chfacfscmulfsupp  20483  chfacfpmmulfsupp  20487  chfacfpmmulgsum2  20489  2ndcctbss  21068  finlocfin  21133  dissnlocfin  21142  locfindis  21143  locfincf  21144  isfild  21472  infil  21477  neifil  21494  flimfcls  21640  istgp2  21705  oppgtmd  21711  oppgtgp  21712  distgp  21713  indistgp  21714  symgtgp  21715  submtmd  21718  subgtgp  21719  qustgplem  21734  prdstmdd  21737  prdstgpd  21738  tlmtgp  21809  isngp4  22226  subgngp  22249  ngptgp  22250  tngngp2  22266  nrgtrg  22304  nrgtdrg  22307  elii2  22543  icopnfcnv  22549  xrhmeo  22553  lebnumii  22573  phtpcer  22602  phtpcerOLD  22603  reparpht  22606  phtpcco2  22607  pcohtpy  22628  pcoass  22632  pcorevlem  22634  pi1cpbl  22652  pi1grplem  22657  isclmi  22685  isncvsngpd  22758  cphsubrglem  22785  cphclm  22797  tchclm  22839  tchcph  22844  clsocv  22857  pjthlem2  23017  ovolf  23057  iundisj2  23124  vitalilem2  23184  vitali  23188  itg2monolem3  23325  dvfsumlem1  23593  dvfsumlem3  23595  mon1puc1p  23714  uc1pmon1p  23715  ply1remlem  23726  drnguc1p  23734  plyaddlem1  23773  coeidlem  23797  aannenlem2  23888  radcnvcl  23975  pilem2  24010  coseq00topi  24058  coseq0negpitopi  24059  tangtx  24061  tanabsge  24062  cosq14gt0  24066  cosq14ge0  24067  cosordlem  24081  sinord  24084  resinf1o  24086  tanord1  24087  tanord  24088  efif1olem3  24094  efsubm  24101  relogrn  24112  logimclad  24123  logrnaddcl  24125  logneg  24138  logcj  24156  argregt0  24160  argrege0  24161  argimgt0  24162  argimlt0  24163  logimul  24164  logneg2  24165  logdmnrp  24187  logcnlem4  24191  dvloglem  24194  logf1o2  24196  efopnlem2  24203  cxpsqrtlem  24248  relogbval  24310  nnlogbexp  24319  relogbcxp  24323  relogbcxpb  24325  asinneg  24413  asinsin  24419  acoscos  24420  acosbnd  24427  atancj  24437  atanlogaddlem  24440  atanlogsublem  24442  atanlogsub  24443  atantan  24450  atanbndlem  24452  atans2  24458  leibpi  24469  scvxcvx  24512  jensenlem2  24514  emcllem7  24528  basellem1  24607  ppisval  24630  chtdif  24684  ppidif  24689  ppiub  24729  chtublem  24736  chtub  24737  lgsdilem2  24858  gausslemma2dlem1a  24890  gausslemma2dlem2  24892  gausslemma2dlem5  24896  gausslemma2dlem6  24897  lgsquadlem1  24905  lgsquadlem2  24906  lgsquadlem3  24907  2lgslem1  24919  2sqlem3  24945  chebbnd1lem1  24958  chebbnd1lem2  24959  chebbnd1lem3  24960  dchrisumlem2  24979  dchrvmasumlem2  24987  dchrvmasumiflem1  24990  dchrisum0flblem2  24998  mulog2sumlem2  25024  logdivbnd  25045  pntpbnd2  25076  pntibndlem1  25078  pntibnd  25082  pntlemc  25084  pntlemg  25087  pntlemq  25090  pntlemf  25094  padicabvf  25120  padicabvcxp  25121  ostth2  25126  ttgcontlem1  25565  axpaschlem  25620  structvtxvallem  25697  nbgraf1olem5  25974  cyclnspth  26159  wwlknred  26251  wwlknredwwlkn  26254  wwlkextproplem3  26271  clwlkisclwwlklem2fv1  26310  clwlkisclwwlklem2fv2  26311  clwlkisclwwlklem2a  26313  clwlkisclwwlklem1  26315  clwwlkel  26321  clwwlkf  26322  wwlkext2clwwlk  26331  clwwisshclwwlem1  26333  clwwisshclwwlem  26334  erclwwlkref  26341  usg2cwwkdifex  26349  clwlkfclwwlk1hash  26369  clwlkfclwwlk  26371  eupath2lem3  26506  extwwlkfablem2  26605  numclwlk2lem2f  26630  frgrareggt1  26643  grpoinvf  26770  strlem3a  28495  hstrlem3a  28503  iundisj2f  28785  fcoinver  28798  ssnnssfz  28937  bcm1n  28941  iundisj2fi  28943  fsumrp0cl  29026  submomnd  29041  lmodslmd  29088  suborng  29146  locfinreflem  29235  locfinref  29236  xrge0iifcnv  29307  xrge0iifiso  29309  xrge0iifhom  29311  esumc  29440  esumle  29447  esumlef  29451  esumpinfsum  29466  esumpcvgval  29467  fiunelros  29564  voliune  29619  volfiniune  29620  sibfinima  29728  eulerpartlemt  29760  fiblem  29787  fibp1  29790  dstrvprob  29860  ballotlemsel1i  29901  ballotlemfrceq  29917  plymulx0  29950  signstfvc  29977  signstfveq0  29980  bnj944  30262  bnj998  30280  bnj1136  30319  bnj1408  30358  erdszelem4  30430  erdszelem8  30434  txsconlem  30476  cvxscon  30479  cvmliftpht  30554  snmlff  30565  elmrsubrn  30671  msrf  30693  mthmpps  30733  sinccvglem  30820  trer  31480  poimirlem6  32585  poimirlem7  32586  poimirlem9  32588  poimirlem17  32596  poimirlem20  32599  poimirlem28  32607  poimirlem29  32608  poimirlem30  32609  poimirlem31  32610  poimirlem32  32611  areacirc  32675  nnubfi  32716  prter1  33182  lkrlss  33400  diaf11N  35356  dibf11N  35468  lclkr  35840  lclkrs  35846  lcfrlem9  35857  lcfr  35892  mapd1o  35955  hdmapf1oN  36175  hgmapf1oN  36213  nacsfix  36293  eldioph2lem1  36341  irrapxlem1  36404  rmxypairf1o  36494  jm2.27a  36590  hbtlem2  36713  hbt  36719  cntzsdrg  36791  mon1pid  36802  mon1psubm  36803  binomcxplemnotnn0  37577  elfzfzo  38429  monoords  38452  fmul01lt1lem2  38652  sumnnodd  38697  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  iblsplit  38858  iblspltprt  38865  itgspltprt  38871  stoweidlem11  38904  stoweidlem17  38910  fourierdlem12  39012  fourierdlem20  39020  fourierdlem25  39025  fourierdlem37  39037  fourierdlem41  39041  fourierdlem48  39047  fourierdlem49  39048  fourierdlem50  39049  fourierdlem54  39053  fourierdlem64  39063  fourierdlem73  39072  fourierdlem79  39078  fourierdlem102  39101  fourierdlem111  39110  fourierdlem114  39113  etransclem23  39150  etransclem48  39175  iccpartiltu  39960  iccpartigtl  39961  iccpartlt  39962  iccpartgt  39965  fmtnoge3  39980  fmtnodvds  39994  odz2prm2pw  40013  fmtnole4prm  40028  lighneallem4b  40064  nnsum4primesevenALTV  40217  bgoldbtbndlem3  40223  lswn0  40242  pfxtrcfv0  40265  pfxeq  40267  pfxtrcfvl  40268  pfx2  40275  pfxccat3  40289  pfxccat3a  40292  2elfz2melfz  40355  elfzlble  40357  fzoopth  40360  pthdadjvtx  40936  pthdlem1  40972  crctcsh1wlkn0lem3  41015  crctcsh1wlkn0lem4  41016  crctcsh1wlkn0lem5  41017  crctcsh1wlkn0lem7  41019  1wlkiswwlks1  41064  wwlksm1edg  41078  wwlksnred  41098  wwlksnredwwlkn  41101  wwlksnextproplem3  41117  clwlkclwwlklem2fv1  41204  clwlkclwwlklem2fv2  41205  clwlkclwwlklem2a  41207  clwlkclwwlklem2  41209  clwwlksel  41221  clwwlksf  41222  wwlksext2clwwlk  41231  wwlksubclwwlks  41232  clwwisshclwwslemlem  41233  clwwisshclwwslem  41234  erclwwlksref  41241  umgr2cwwkdifex  41249  clwlksfclwwlk  41269  eucrctshift  41411  av-extwwlkfablem2  41510  av-numclwlk2lem2f  41533  av-frgrareggt1  41547  ringrng  41669  isringrng  41671  lidlrng  41717  ssnn0ssfz  41920  lmod1  42075  elfzolborelfzop1  42103  nnolog2flm1  42182