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  7320  limuni3  7837  onfununi  8337  smores2  8350  smoiso  8358  oelimcl  8596  iserd  8725  resixp  8923  undifixp  8924  alephval3  10101  canthwelem  10641  canthwe  10642  r1limwun  10727  wunex2  10729  tskcard  10772  gruina  10809  eluzmn  12825  eluzuzle  12827  uztrn  12836  eluzadd  12847  eluzsub  12848  subeluzsub  12855  nn0pzuz  12885  zsupss  12917  nn0ge2m1nnALT  12922  xov1plusxeqvd  13471  ige2m1fz  13587  0elfz  13594  uzsubfz0  13605  elfzmlbm  13607  difelfzle  13610  difelfznle  13611  fvffz0  13615  elfzolt2b  13639  elfzolt3b  13640  elfzouz2  13643  fzossrbm1  13657  elfzo0  13669  eluzgtdifelfzo  13690  elfzodifsumelfzo  13694  fzonn0p1  13705  fzonn0p1p1  13707  fzo0sn0fzo1  13717  ssfzo12bi  13723  ubmelm1fzo  13724  elfzonelfzo  13730  fzosplitprm1  13738  fzostep1  13744  fvinim0ffz  13747  flword2  13774  uzsup  13824  modfzo0difsn  13904  modsumfzodifsn  13905  fsuppmapnn0fiub  13952  suppssfz  13955  1elfz0hash  14346  fzsdom2  14384  ccatrn  14535  ccat2s1fvw  14584  pfxn0  14632  pfxtrcfv0  14640  pfxtrcfvl  14643  swrdswrd  14651  swrdccatin1  14671  pfxccat3  14680  pfxccat3a  14684  repswswrd  14730  cshwidxmod  14749  cshw1  14768  cshwcsh2id  14775  swrds2  14887  pfx2  14894  2swrd2eqwrdeq  14900  ccat2s1fvwALT  14902  rexuzre  15295  limsupgre  15421  rlimclim1  15485  rlimclim  15486  climrlim2  15487  isercolllem1  15607  isercoll  15610  climcndslem1  15791  fallfacval4  15983  tanhbnd  16100  sinbnd2  16121  cosbnd2  16122  rpnnen2lem12  16164  nn0o  16322  bitsfzolem  16371  bitsfzo  16372  bitsmod  16373  bitsfi  16374  bitsinv1lem  16378  bitsinv1  16379  smueqlem  16427  dvdsnprmd  16623  2mulprm  16626  hashgcdlem  16717  prm23lt5  16743  zgz  16862  gznegcl  16864  gzcjcl  16865  gzaddcl  16866  gzmulcl  16867  vdwlem9  16918  prmgaplem3  16982  prmgaplem4  16983  cshwshashlem2  17026  setsstruct2  17103  ismred  17542  isfuncd  17811  homdmcoa  18013  isdrs2  18255  fpwipodrs  18489  ipodrsima  18490  sgrp2rid2ex  18804  subgid  19002  issubg2  19015  subsubg  19023  gaorber  19166  orbsta  19171  pmtrfconj  19328  psgnunilem2  19357  psgnunilem3  19358  psgnunilem4  19359  pgpfi1  19457  subgpgp  19459  pgpssslw  19476  subgslw  19478  sylow2alem2  19480  fislw  19487  sylow3lem3  19491  efgs1  19597  efgsp1  19599  efgsres  19600  efgredleme  19605  efgcpbllemb  19617  lt6abl  19757  telgsumfzs  19851  ablfac1eu  19937  isringd  20098  ringsrg  20102  ring1  20115  prdsringd  20127  subrgsubg  20361  sdrgid  20400  cntzsdrg  20410  subdrgint  20411  sdrgint  20412  islmodd  20469  islssd  20538  islss4  20565  dflidl2lem  20834  gzrngunit  21003  expmhm  21006  zringunit  21027  prmirredlem  21033  znidomb  21108  isphld  21198  ocvocv  21215  ocvlss  21216  frlmlbs  21343  gsummoncoe1  21819  mp2pm2mplem4  22302  chfacfisf  22347  chfacfisfcpmat  22348  chfacfscmulfsupp  22352  chfacfpmmulfsupp  22356  chfacfpmmulgsum2  22358  2ndcctbss  22950  finlocfin  23015  dissnlocfin  23024  locfindis  23025  locfincf  23026  isfild  23353  infil  23358  neifil  23375  flimfcls  23521  istgp2  23586  oppgtmd  23592  oppgtgp  23593  distgp  23594  indistgp  23595  efmndtmd  23596  submtmd  23599  subgtgp  23600  symgtgp  23601  qustgplem  23616  prdstmdd  23619  prdstgpd  23620  tlmtgp  23691  isngp4  24112  subgngp  24135  ngptgp  24136  tngngp2  24160  nrgtrg  24198  nrgtdrg  24201  elii2  24443  icopnfcnv  24449  xrhmeo  24453  lebnumii  24473  phtpcer  24502  reparpht  24505  phtpcco2  24506  pcohtpy  24527  pcoass  24531  pcorevlem  24533  isclmi  24584  isncvsngpd  24658  cphsubrglem  24685  cphclm  24697  phclm  24740  tcphcph  24745  clsocv  24758  cphsscph  24759  cmslssbn  24880  pjthlem2  24946  ovolf  24990  iundisj2  25057  vitalilem2  25117  vitali  25121  itg2monolem3  25261  dvfsumlem1  25534  dvfsumlem3  25536  mon1puc1p  25659  uc1pmon1p  25660  ply1remlem  25671  drnguc1p  25679  plyaddlem1  25718  coeidlem  25742  aannenlem2  25833  radcnvcl  25920  pilem2  25955  coseq00topi  26003  coseq0negpitopi  26004  tangtx  26006  tanabsge  26007  cosq14gt0  26011  cosq14ge0  26012  cosq34lt1  26027  cosordlem  26030  cos0pilt1  26032  sinord  26034  resinf1o  26036  tanord1  26037  tanord  26038  efif1olem3  26044  efsubm  26051  relogrn  26061  logimclad  26072  logrnaddcl  26074  logneg  26087  logcj  26105  argregt0  26109  argrege0  26110  argimgt0  26111  argimlt0  26112  logimul  26113  logneg2  26114  logdmnrp  26140  logcnlem4  26144  dvloglem  26147  logf1o2  26149  efopnlem2  26156  cxpsqrtlem  26201  relogbval  26266  nnlogbexp  26275  relogbcxp  26279  relogbcxpb  26281  logbgt0b  26287  asinneg  26380  asinsin  26386  acoscos  26387  acosbnd  26394  atancj  26404  atanlogaddlem  26407  atanlogsublem  26409  atanlogsub  26410  atantan  26417  atanbndlem  26419  atans2  26425  leibpi  26436  scvxcvx  26479  jensenlem2  26481  emcllem7  26495  basellem1  26574  ppisval  26597  chtdif  26651  ppidif  26656  ppiub  26696  chtublem  26703  chtub  26704  lgsdilem2  26825  gausslemma2dlem1a  26857  gausslemma2dlem2  26859  gausslemma2dlem5  26863  gausslemma2dlem6  26864  lgsquadlem1  26872  lgsquadlem2  26873  lgsquadlem3  26874  2lgslem1  26886  2sqlem3  26912  chebbnd1lem1  26961  chebbnd1lem2  26962  chebbnd1lem3  26963  dchrisumlem2  26982  dchrvmasumlem2  26990  dchrvmasumiflem1  26993  dchrisum0flblem2  27001  mulog2sumlem2  27027  logdivbnd  27048  pntpbnd2  27079  pntibndlem1  27081  pntibnd  27085  pntlemc  27087  pntlemg  27090  pntlemq  27093  pntlemf  27097  padicabvf  27123  padicabvcxp  27124  ostth2  27129  noextend  27158  noextendseq  27159  nosupno  27195  noinfno  27210  ttgcontlem1  28131  axpaschlem  28187  nbgr2vtx1edg  28596  nbuhgr2vtx1edgb  28598  cusgrexi  28689  structtocusgr  28692  pthdadjvtx  28976  pthdlem1  29012  pthd  29015  crctcshwlkn0lem3  29055  crctcshwlkn0lem4  29056  crctcshwlkn0lem5  29057  crctcshwlkn0lem7  29059  wlkiswwlks1  29110  wwlksm1edg  29124  wwlksnred  29135  wwlksnredwwlkn  29138  wwlksnextproplem3  29154  clwlkclwwlklem2fv1  29237  clwlkclwwlklem2fv2  29238  clwlkclwwlklem2a  29240  clwlkclwwlklem2  29242  clwwisshclwwslemlem  29255  clwwisshclwwslem  29256  erclwwlkref  29262  clwwlkel  29288  clwwlkf  29289  wwlksext2clwwlk  29299  wwlksubclwwlk  29300  umgr2cwwkdifex  29307  1pthd  29385  eucrctshift  29485  dlwwlknondlwlknonf1olem1  29606  numclwlk2lem2f  29619  frgrreggt1  29635  grpoinvf  29772  strlem3a  31492  hstrlem3a  31500  iundisj2f  31808  fcoinver  31822  fresf1o  31842  ssnnssfz  31985  bcm1n  31993  iundisj2fi  31995  fsumrp0cl  32183  submomnd  32215  cycpmco2lem6  32277  lmodslmd  32336  fldgensdrg  32392  suborng  32421  intlidl  32524  rhmpreimaidl  32525  idlinsubrg  32537  rhmimaidl  32538  ssmxidllem  32577  minplyirred  32758  algextdeglem1  32760  locfinreflem  32808  locfinref  32809  xrge0iifcnv  32901  xrge0iifiso  32903  xrge0iifhom  32905  esumc  33037  esumle  33044  esumlef  33048  esumpinfsum  33063  esumpcvgval  33064  fiunelros  33160  voliune  33215  volfiniune  33216  sibfinima  33326  eulerpartlemt  33358  fiblem  33385  fibp1  33388  dstrvprob  33458  ballotlemsel1i  33499  ballotlemfrceq  33515  plymulx0  33546  signstfvc  33573  signstfveq0  33576  bnj944  33937  bnj998  33956  bnj1136  33996  bnj1408  34035  erdszelem4  34173  erdszelem8  34177  txsconnlem  34219  cvxsconn  34222  cvmliftpht  34297  snmlff  34308  elmrsubrn  34499  msrf  34521  mthmpps  34561  sinccvglem  34645  trer  35189  poimirlem6  36482  poimirlem7  36483  poimirlem9  36485  poimirlem17  36493  poimirlem20  36496  poimirlem28  36504  poimirlem29  36505  poimirlem30  36506  poimirlem31  36507  poimirlem32  36508  areacirc  36569  nnubfi  36606  prter1  37737  lkrlss  37953  diaf11N  39908  dibf11N  40020  lclkr  40392  lclkrs  40398  lcfrlem9  40409  lcfr  40444  mapd1o  40507  hdmapf1oN  40724  hgmapf1oN  40762  frlmvscadiccat  41077  sn-inelr  41334  nacsfix  41435  eldioph2lem1  41483  irrapxlem1  41545  rmxypairf1o  41635  jm2.27a  41729  hbtlem2  41851  hbt  41857  mon1pid  41932  mon1psubm  41933  onnog  42165  pren2d  42292  binomcxplemnotnn0  43100  elixpconstg  43763  elfzfzo  43972  monoords  43993  elfzod  44096  eluzd  44105  fmul01lt1lem2  44287  sumnnodd  44332  ioodvbdlimc1lem2  44634  ioodvbdlimc2lem  44636  iblsplit  44668  iblspltprt  44675  itgspltprt  44681  stoweidlem11  44713  stoweidlem17  44719  fourierdlem12  44821  fourierdlem20  44829  fourierdlem25  44834  fourierdlem37  44846  fourierdlem41  44850  fourierdlem48  44856  fourierdlem49  44857  fourierdlem50  44858  fourierdlem54  44862  fourierdlem64  44872  fourierdlem73  44881  fourierdlem79  44887  fourierdlem102  44910  fourierdlem111  44919  fourierdlem114  44922  etransclem23  44959  etransclem48  44984  2elfz2melfz  46012  elfzlble  46014  fzoopth  46021  iccpartiltu  46076  iccpartigtl  46077  iccpartlt  46078  iccpartgt  46081  lswn0  46098  fmtnoge3  46184  fmtnodvds  46198  odz2prm2pw  46217  fmtnole4prm  46232  lighneallem4b  46263  mogoldbb  46439  nnsum4primesevenALTV  46455  bgoldbtbndlem3  46461  ringrng  46641  isringrng  46643  isrngd  46658  prdsrngd  46663  subrngid  46712  subrngsubg  46715  issubrng2  46721  subsubrng  46726  rnglidl0  46734  rnglidl1  46735  rnglidlrng  46740  rng2idlsubrng  46741  ssnn0ssfz  46978  lmod1  47126  elfzolborelfzop1  47153  nnolog2flm1  47229