Theorem syl3anbrc 1323

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

Syntax hints:   → wi 4   ↔ wb 198   ∧ w3a 1068

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 199  df-an 388  df-3an 1070

This theorem is referenced by:  soisores  6903  limuni3  7383  onfununi  7782  smores2  7795  smoiso  7803  oelimcl  8027  iserd  8115  resixp  8294  undifixp  8295  alephval3  9330  canthwelem  9870  canthwe  9871  r1limwun  9956  wunex2  9958  tskcard  10001  gruina  10038  eluzmn  12065  eluzuzle  12067  uztrn  12075  subeluzsub  12089  nn0pzuz  12119  zsupss  12151  nn0ge2m1nnALT  12156  xov1plusxeqvd  12700  ssfzunsnext  12768  ige2m1fz  12813  0elfz  12820  uzsubfz0  12831  elfzmlbm  12833  difelfzle  12836  difelfznle  12837  fvffz0  12841  elfzolt2b  12865  elfzolt3b  12866  elfzouz2  12868  fzossrbm1  12881  elfzo0  12893  eluzgtdifelfzo  12914  elfzodifsumelfzo  12918  fzonn0p1  12929  fzonn0p1p1  12931  elfzom1p1elfzo  12932  fzo0sn0fzo1  12941  ssfzo12bi  12947  ubmelm1fzo  12948  elfzonelfzo  12954  fzosplitprm1  12962  fzostep1  12968  fvinim0ffz  12971  flword2  12998  uzsup  13046  modfzo0difsn  13126  modsumfzodifsn  13127  fsuppmapnn0fiub  13174  suppssfz  13177  1elfz0hash  13564  fzsdom2  13602  ccatrn  13752  swrdn0OLD  13820  swrdtrcfvOLD  13833  swrdtrcfv0OLD  13834  swrdeqOLD  13836  swrdtrcfvlOLD  13843  pfxn0  13868  pfxtrcfv0  13876  pfxeq  13878  pfxtrcfvl  13879  swrdswrd  13887  swrdccatwrdOLD  13903  wrdeqs1catOLD  13913  swrdccatin1  13924  pfxccat3  13936  swrdccat3OLD  13937  pfxccat3a  13942  swrdccatidOLD  13948  repswswrd  14003  cshwidxmod  14027  cshw1  14046  cshwcsh2id  14052  swrds2  14164  pfx2  14171  2swrd2eqwrdeq  14177  2swrd2eqwrdeqOLD  14178  ccat2s1fvwALT  14180  rexuzre  14573  limsupgre  14699  rlimclim1  14763  rlimclim  14764  climrlim2  14765  isercolllem1  14882  isercoll  14885  climcndslem1  15064  fallfacval4  15257  tanhbnd  15374  sinbnd2  15395  cosbnd2  15396  rpnnen2lem12  15438  nn0o  15594  bitsfzolem  15643  bitsfzo  15644  bitsmod  15645  bitsfi  15646  bitsinv1lem  15650  bitsinv1  15651  smueqlem  15699  dvdsnprmd  15890  2mulprm  15893  hashgcdlem  15981  prm23lt5  16007  zgz  16125  gznegcl  16127  gzcjcl  16128  gzaddcl  16129  gzmulcl  16130  vdwlem9  16181  prmgaplem3  16245  prmgaplem4  16246  cshwshashlem2  16286  setsstruct2  16377  ismred  16731  isfuncd  16993  homdmcoa  17185  isdrs2  17407  fpwipodrs  17632  ipodrsima  17633  sgrp2rid2ex  17883  subgid  18065  issubg2  18078  subsubg  18086  gaorber  18209  orbsta  18214  pmtrfconj  18355  psgnunilem2  18385  psgnunilem3  18386  psgnunilem4  18387  pgpfi1  18481  subgpgp  18483  pgpssslw  18500  subgslw  18502  sylow2alem2  18504  fislw  18511  sylow3lem3  18515  efgs1  18619  efgsp1  18621  efgsres  18622  efgsresOLD  18623  efgredleme  18628  efgcpbllemb  18641  lt6abl  18769  telgsumfzs  18859  ablfac1eu  18945  isringd  19058  ringsrg  19062  ring1  19075  prdsringd  19085  subrgsubg  19264  sdrgid  19297  cntzsdrg  19303  subdrgint  19304  sdrgint  19305  islmodd  19362  islssd  19429  islss4  19456  gsummoncoe1  20175  gzrngunit  20313  expmhm  20316  zringunit  20337  prmirredlem  20342  znidomb  20410  isphld  20500  ocvocv  20517  ocvlss  20518  frlmlbs  20643  mp2pm2mplem4  21121  chfacfisf  21166  chfacfisfcpmat  21167  chfacfscmulfsupp  21171  chfacfpmmulfsupp  21175  chfacfpmmulgsum2  21177  2ndcctbss  21767  finlocfin  21832  dissnlocfin  21841  locfindis  21842  locfincf  21843  isfild  22170  infil  22175  neifil  22192  flimfcls  22338  istgp2  22403  oppgtmd  22409  oppgtgp  22410  distgp  22411  indistgp  22412  symgtgp  22413  submtmd  22416  subgtgp  22417  qustgplem  22432  prdstmdd  22435  prdstgpd  22436  tlmtgp  22507  isngp4  22924  subgngp  22947  ngptgp  22948  tngngp2  22964  nrgtrg  23002  nrgtdrg  23005  elii2  23243  icopnfcnv  23249  xrhmeo  23253  lebnumii  23273  phtpcer  23302  reparpht  23305  phtpcco2  23306  pcohtpy  23327  pcoass  23331  pcorevlem  23333  isclmi  23384  isncvsngpd  23457  cphsubrglem  23484  cphclm  23496  phclm  23538  tcphcph  23543  clsocv  23556  cphsscph  23557  cmslssbn  23678  pjthlem2  23744  ovolf  23786  iundisj2  23853  vitalilem2  23913  vitali  23917  itg2monolem3  24056  dvfsumlem1  24326  dvfsumlem3  24328  mon1puc1p  24447  uc1pmon1p  24448  ply1remlem  24459  drnguc1p  24467  plyaddlem1  24506  coeidlem  24530  aannenlem2  24621  radcnvcl  24708  pilem2  24743  coseq00topi  24791  coseq0negpitopi  24792  tangtx  24794  tanabsge  24795  cosq14gt0  24799  cosq14ge0  24800  cosordlem  24816  sinord  24819  resinf1o  24821  tanord1  24822  tanord  24823  efif1olem3  24829  efsubm  24836  relogrn  24846  logimclad  24857  logrnaddcl  24859  logneg  24872  logcj  24890  argregt0  24894  argrege0  24895  argimgt0  24896  argimlt0  24897  logimul  24898  logneg2  24899  logdmnrp  24925  logcnlem4  24929  dvloglem  24932  logf1o2  24934  efopnlem2  24941  cxpsqrtlem  24986  relogbval  25051  nnlogbexp  25060  relogbcxp  25064  relogbcxpb  25066  logbgt0b  25072  asinneg  25165  asinsin  25171  acoscos  25172  acosbnd  25179  atancj  25189  atanlogaddlem  25192  atanlogsublem  25194  atanlogsub  25195  atantan  25202  atanbndlem  25204  atans2  25210  leibpi  25222  scvxcvx  25265  jensenlem2  25267  emcllem7  25281  basellem1  25360  ppisval  25383  chtdif  25437  ppidif  25442  ppiub  25482  chtublem  25489  chtub  25490  lgsdilem2  25611  gausslemma2dlem1a  25643  gausslemma2dlem2  25645  gausslemma2dlem5  25649  gausslemma2dlem6  25650  lgsquadlem1  25658  lgsquadlem2  25659  lgsquadlem3  25660  2lgslem1  25672  2sqlem3  25698  chebbnd1lem1  25747  chebbnd1lem2  25748  chebbnd1lem3  25749  dchrisumlem2  25768  dchrvmasumlem2  25776  dchrvmasumiflem1  25779  dchrisum0flblem2  25787  mulog2sumlem2  25813  logdivbnd  25834  pntpbnd2  25865  pntibndlem1  25867  pntibnd  25871  pntlemc  25873  pntlemg  25876  pntlemq  25879  pntlemf  25883  padicabvf  25909  padicabvcxp  25910  ostth2  25915  ttgcontlem1  26374  axpaschlem  26429  nbgr2vtx1edg  26835  nbuhgr2vtx1edgb  26837  cusgrexi  26928  structtocusgr  26931  pthdadjvtx  27219  pthdlem1  27255  pthd  27258  crctcshwlkn0lem3  27298  crctcshwlkn0lem4  27299  crctcshwlkn0lem5  27300  crctcshwlkn0lem7  27302  wlkiswwlks1  27353  wwlksm1edg  27367  wwlksm1edgOLD  27368  wwlksnred  27379  wwlksnredOLD  27380  wwlksnredwwlkn  27384  wwlksnredwwlknOLD  27385  wwlksnextproplem3  27413  wwlksnextproplem3OLD  27414  clwlkclwwlklem2fv1  27501  clwlkclwwlklem2fv2  27502  clwlkclwwlklem2a  27504  clwlkclwwlklem2  27506  clwwisshclwwslemlem  27528  clwwisshclwwslem  27529  erclwwlkref  27535  clwwlkel  27563  clwwlkfOLD  27564  clwwlkf  27569  wwlksext2clwwlk  27580  wwlksubclwwlk  27581  wwlksubclwwlkOLD  27582  umgr2cwwkdifex  27589  1pthd  27672  eucrctshift  27773  dlwwlknondlwlknonf1olem1  27914  dlwwlknonclwlknonf1olem1OLD  27915  numclwlk2lem2f  27930  numclwlk2lem2fOLD  27933  frgrreggt1  27950  grpoinvf  28086  strlem3a  29810  hstrlem3a  29818  iundisj2f  30106  fcoinver  30121  fresf1o  30139  ssnnssfz  30269  bcm1n  30274  iundisj2fi  30276  fsumrp0cl  30420  submomnd  30435  lmodslmd  30504  suborng  30573  locfinreflem  30754  locfinref  30755  xrge0iifcnv  30826  xrge0iifiso  30828  xrge0iifhom  30830  esumc  30960  esumle  30967  esumlef  30971  esumpinfsum  30986  esumpcvgval  30987  fiunelros  31084  voliune  31139  volfiniune  31140  sibfinima  31248  eulerpartlemt  31280  fiblem  31308  fibp1  31311  dstrvprob  31381  ballotlemsel1i  31422  ballotlemfrceq  31438  plymulx0  31469  signstfvc  31497  signstfveq0  31500  signstfveq0OLD  31501  bnj944  31863  bnj998  31881  bnj1136  31920  bnj1408  31959  erdszelem4  32032  erdszelem8  32036  txsconnlem  32078  cvxsconn  32081  cvmliftpht  32156  snmlff  32167  elmrsubrn  32293  msrf  32315  mthmpps  32355  sinccvglem  32441  noextend  32700  noextendseq  32701  nosupno  32730  trer  33191  poimirlem6  34345  poimirlem7  34346  poimirlem9  34348  poimirlem17  34356  poimirlem20  34359  poimirlem28  34367  poimirlem29  34368  poimirlem30  34369  poimirlem31  34370  poimirlem32  34371  areacirc  34434  nnubfi  34473  prter1  35466  lkrlss  35682  diaf11N  37636  dibf11N  37748  lclkr  38120  lclkrs  38126  lcfrlem9  38137  lcfr  38172  mapd1o  38235  hdmapf1oN  38452  hgmapf1oN  38490  frlmvscadiccat  38588  nacsfix  38710  eldioph2lem1  38758  irrapxlem1  38821  rmxypairf1o  38910  jm2.27a  39004  hbtlem2  39126  hbt  39132  mon1pid  39207  mon1psubm  39208  binomcxplemnotnn0  40110  elixpconstg  40782  elfzfzo  40977  monoords  40999  elfzod  41109  eluzd  41119  fmul01lt1lem2  41303  sumnnodd  41348  ioodvbdlimc1lem2  41653  ioodvbdlimc2lem  41655  iblsplit  41687  iblspltprt  41694  itgspltprt  41700  stoweidlem11  41733  stoweidlem17  41739  fourierdlem12  41841  fourierdlem20  41849  fourierdlem25  41854  fourierdlem37  41866  fourierdlem41  41870  fourierdlem48  41876  fourierdlem49  41877  fourierdlem50  41878  fourierdlem54  41882  fourierdlem64  41892  fourierdlem73  41901  fourierdlem79  41907  fourierdlem102  41930  fourierdlem111  41939  fourierdlem114  41942  etransclem23  41979  etransclem48  42004  2elfz2melfz  42930  elfzlble  42932  fzoopth  42939  iccpartiltu  42960  iccpartigtl  42961  iccpartlt  42962  iccpartgt  42965  lswn0  42982  fmtnoge3  43066  fmtnodvds  43080  odz2prm2pw  43099  fmtnole4prm  43114  lighneallem4b  43148  mogoldbb  43324  nnsum4primesevenALTV  43340  bgoldbtbndlem3  43346  ringrng  43520  isringrng  43522  lidlrng  43568  ssnn0ssfz  43767  lmod1  43920  elfzolborelfzop1  43948  nnolog2flm1  44024