Theorem syl3anbrc 1341

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

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

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 396  df-3an 1087

This theorem is referenced by:  soisores  7178  limuni3  7674  onfununi  8143  smores2  8156  smoiso  8164  oelimcl  8393  iserd  8482  resixp  8679  undifixp  8680  alephval3  9797  canthwelem  10337  canthwe  10338  r1limwun  10423  wunex2  10425  tskcard  10468  gruina  10505  eluzmn  12518  eluzuzle  12520  uztrn  12529  subeluzsub  12544  nn0pzuz  12574  zsupss  12606  nn0ge2m1nnALT  12611  xov1plusxeqvd  13159  ige2m1fz  13275  0elfz  13282  uzsubfz0  13293  elfzmlbm  13295  difelfzle  13298  difelfznle  13299  fvffz0  13303  elfzolt2b  13327  elfzolt3b  13328  elfzouz2  13330  fzossrbm1  13344  elfzo0  13356  eluzgtdifelfzo  13377  elfzodifsumelfzo  13381  fzonn0p1  13392  fzonn0p1p1  13394  fzo0sn0fzo1  13404  ssfzo12bi  13410  ubmelm1fzo  13411  elfzonelfzo  13417  fzosplitprm1  13425  fzostep1  13431  fvinim0ffz  13434  flword2  13461  uzsup  13511  modfzo0difsn  13591  modsumfzodifsn  13592  fsuppmapnn0fiub  13639  suppssfz  13642  1elfz0hash  14033  fzsdom2  14071  ccatrn  14222  ccat2s1fvw  14277  ccat2s1fvwOLD  14278  pfxn0  14327  pfxtrcfv0  14335  pfxtrcfvl  14338  swrdswrd  14346  swrdccatin1  14366  pfxccat3  14375  pfxccat3a  14379  repswswrd  14425  cshwidxmod  14444  cshw1  14463  cshwcsh2id  14469  swrds2  14581  pfx2  14588  2swrd2eqwrdeq  14594  ccat2s1fvwALT  14597  ccat2s1fvwALTOLD  14598  rexuzre  14992  limsupgre  15118  rlimclim1  15182  rlimclim  15183  climrlim2  15184  isercolllem1  15304  isercoll  15307  climcndslem1  15489  fallfacval4  15681  tanhbnd  15798  sinbnd2  15819  cosbnd2  15820  rpnnen2lem12  15862  nn0o  16020  bitsfzolem  16069  bitsfzo  16070  bitsmod  16071  bitsfi  16072  bitsinv1lem  16076  bitsinv1  16077  smueqlem  16125  dvdsnprmd  16323  2mulprm  16326  hashgcdlem  16417  prm23lt5  16443  zgz  16562  gznegcl  16564  gzcjcl  16565  gzaddcl  16566  gzmulcl  16567  vdwlem9  16618  prmgaplem3  16682  prmgaplem4  16683  cshwshashlem2  16726  setsstruct2  16803  ismred  17228  isfuncd  17496  homdmcoa  17698  isdrs2  17939  fpwipodrs  18173  ipodrsima  18174  sgrp2rid2ex  18481  subgid  18672  issubg2  18685  subsubg  18693  gaorber  18829  orbsta  18834  pmtrfconj  18989  psgnunilem2  19018  psgnunilem3  19019  psgnunilem4  19020  pgpfi1  19115  subgpgp  19117  pgpssslw  19134  subgslw  19136  sylow2alem2  19138  fislw  19145  sylow3lem3  19149  efgs1  19256  efgsp1  19258  efgsres  19259  efgredleme  19264  efgcpbllemb  19276  lt6abl  19411  telgsumfzs  19505  ablfac1eu  19591  isringd  19739  ringsrg  19743  ring1  19756  prdsringd  19766  subrgsubg  19945  sdrgid  19979  cntzsdrg  19985  subdrgint  19986  sdrgint  19987  islmodd  20044  islssd  20112  islss4  20139  gzrngunit  20576  expmhm  20579  zringunit  20600  prmirredlem  20606  znidomb  20681  isphld  20771  ocvocv  20788  ocvlss  20789  frlmlbs  20914  gsummoncoe1  21385  mp2pm2mplem4  21866  chfacfisf  21911  chfacfisfcpmat  21912  chfacfscmulfsupp  21916  chfacfpmmulfsupp  21920  chfacfpmmulgsum2  21922  2ndcctbss  22514  finlocfin  22579  dissnlocfin  22588  locfindis  22589  locfincf  22590  isfild  22917  infil  22922  neifil  22939  flimfcls  23085  istgp2  23150  oppgtmd  23156  oppgtgp  23157  distgp  23158  indistgp  23159  efmndtmd  23160  submtmd  23163  subgtgp  23164  symgtgp  23165  qustgplem  23180  prdstmdd  23183  prdstgpd  23184  tlmtgp  23255  isngp4  23674  subgngp  23697  ngptgp  23698  tngngp2  23722  nrgtrg  23760  nrgtdrg  23763  elii2  24005  icopnfcnv  24011  xrhmeo  24015  lebnumii  24035  phtpcer  24064  reparpht  24067  phtpcco2  24068  pcohtpy  24089  pcoass  24093  pcorevlem  24095  isclmi  24146  isncvsngpd  24219  cphsubrglem  24246  cphclm  24258  phclm  24301  tcphcph  24306  clsocv  24319  cphsscph  24320  cmslssbn  24441  pjthlem2  24507  ovolf  24551  iundisj2  24618  vitalilem2  24678  vitali  24682  itg2monolem3  24822  dvfsumlem1  25095  dvfsumlem3  25097  mon1puc1p  25220  uc1pmon1p  25221  ply1remlem  25232  drnguc1p  25240  plyaddlem1  25279  coeidlem  25303  aannenlem2  25394  radcnvcl  25481  pilem2  25516  coseq00topi  25564  coseq0negpitopi  25565  tangtx  25567  tanabsge  25568  cosq14gt0  25572  cosq14ge0  25573  cosq34lt1  25588  cosordlem  25591  cos0pilt1  25593  sinord  25595  resinf1o  25597  tanord1  25598  tanord  25599  efif1olem3  25605  efsubm  25612  relogrn  25622  logimclad  25633  logrnaddcl  25635  logneg  25648  logcj  25666  argregt0  25670  argrege0  25671  argimgt0  25672  argimlt0  25673  logimul  25674  logneg2  25675  logdmnrp  25701  logcnlem4  25705  dvloglem  25708  logf1o2  25710  efopnlem2  25717  cxpsqrtlem  25762  relogbval  25827  nnlogbexp  25836  relogbcxp  25840  relogbcxpb  25842  logbgt0b  25848  asinneg  25941  asinsin  25947  acoscos  25948  acosbnd  25955  atancj  25965  atanlogaddlem  25968  atanlogsublem  25970  atanlogsub  25971  atantan  25978  atanbndlem  25980  atans2  25986  leibpi  25997  scvxcvx  26040  jensenlem2  26042  emcllem7  26056  basellem1  26135  ppisval  26158  chtdif  26212  ppidif  26217  ppiub  26257  chtublem  26264  chtub  26265  lgsdilem2  26386  gausslemma2dlem1a  26418  gausslemma2dlem2  26420  gausslemma2dlem5  26424  gausslemma2dlem6  26425  lgsquadlem1  26433  lgsquadlem2  26434  lgsquadlem3  26435  2lgslem1  26447  2sqlem3  26473  chebbnd1lem1  26522  chebbnd1lem2  26523  chebbnd1lem3  26524  dchrisumlem2  26543  dchrvmasumlem2  26551  dchrvmasumiflem1  26554  dchrisum0flblem2  26562  mulog2sumlem2  26588  logdivbnd  26609  pntpbnd2  26640  pntibndlem1  26642  pntibnd  26646  pntlemc  26648  pntlemg  26651  pntlemq  26654  pntlemf  26658  padicabvf  26684  padicabvcxp  26685  ostth2  26690  ttgcontlem1  27155  axpaschlem  27211  nbgr2vtx1edg  27620  nbuhgr2vtx1edgb  27622  cusgrexi  27713  structtocusgr  27716  pthdadjvtx  27999  pthdlem1  28035  pthd  28038  crctcshwlkn0lem3  28078  crctcshwlkn0lem4  28079  crctcshwlkn0lem5  28080  crctcshwlkn0lem7  28082  wlkiswwlks1  28133  wwlksm1edg  28147  wwlksnred  28158  wwlksnredwwlkn  28161  wwlksnextproplem3  28177  clwlkclwwlklem2fv1  28260  clwlkclwwlklem2fv2  28261  clwlkclwwlklem2a  28263  clwlkclwwlklem2  28265  clwwisshclwwslemlem  28278  clwwisshclwwslem  28279  erclwwlkref  28285  clwwlkel  28311  clwwlkf  28312  wwlksext2clwwlk  28322  wwlksubclwwlk  28323  umgr2cwwkdifex  28330  1pthd  28408  eucrctshift  28508  dlwwlknondlwlknonf1olem1  28629  numclwlk2lem2f  28642  frgrreggt1  28658  grpoinvf  28795  strlem3a  30515  hstrlem3a  30523  iundisj2f  30830  fcoinver  30847  fresf1o  30867  ssnnssfz  31010  bcm1n  31018  iundisj2fi  31020  fsumrp0cl  31206  submomnd  31238  cycpmco2lem6  31300  lmodslmd  31359  suborng  31416  intlidl  31504  rhmpreimaidl  31505  idlinsubrg  31510  rhmimaidl  31511  ssmxidllem  31543  locfinreflem  31692  locfinref  31693  xrge0iifcnv  31785  xrge0iifiso  31787  xrge0iifhom  31789  esumc  31919  esumle  31926  esumlef  31930  esumpinfsum  31945  esumpcvgval  31946  fiunelros  32042  voliune  32097  volfiniune  32098  sibfinima  32206  eulerpartlemt  32238  fiblem  32265  fibp1  32268  dstrvprob  32338  ballotlemsel1i  32379  ballotlemfrceq  32395  plymulx0  32426  signstfvc  32453  signstfveq0  32456  bnj944  32818  bnj998  32837  bnj1136  32877  bnj1408  32916  erdszelem4  33056  erdszelem8  33060  txsconnlem  33102  cvxsconn  33105  cvmliftpht  33180  snmlff  33191  elmrsubrn  33382  msrf  33404  mthmpps  33444  sinccvglem  33530  noextend  33796  noextendseq  33797  nosupno  33833  noinfno  33848  trer  34432  poimirlem6  35710  poimirlem7  35711  poimirlem9  35713  poimirlem17  35721  poimirlem20  35724  poimirlem28  35732  poimirlem29  35733  poimirlem30  35734  poimirlem31  35735  poimirlem32  35736  areacirc  35797  nnubfi  35835  prter1  36820  lkrlss  37036  diaf11N  38990  dibf11N  39102  lclkr  39474  lclkrs  39480  lcfrlem9  39491  lcfr  39526  mapd1o  39589  hdmapf1oN  39806  hgmapf1oN  39844  frlmvscadiccat  40163  sn-inelr  40356  nacsfix  40450  eldioph2lem1  40498  irrapxlem1  40560  rmxypairf1o  40649  jm2.27a  40743  hbtlem2  40865  hbt  40871  mon1pid  40946  mon1psubm  40947  pren2d  41052  binomcxplemnotnn0  41863  elixpconstg  42528  elfzfzo  42704  monoords  42726  elfzod  42830  eluzd  42839  fmul01lt1lem2  43016  sumnnodd  43061  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  iblsplit  43397  iblspltprt  43404  itgspltprt  43410  stoweidlem11  43442  stoweidlem17  43448  fourierdlem12  43550  fourierdlem20  43558  fourierdlem25  43563  fourierdlem37  43575  fourierdlem41  43579  fourierdlem48  43585  fourierdlem49  43586  fourierdlem50  43587  fourierdlem54  43591  fourierdlem64  43601  fourierdlem73  43610  fourierdlem79  43616  fourierdlem102  43639  fourierdlem111  43648  fourierdlem114  43651  etransclem23  43688  etransclem48  43713  2elfz2melfz  44698  elfzlble  44700  fzoopth  44707  iccpartiltu  44762  iccpartigtl  44763  iccpartlt  44764  iccpartgt  44767  lswn0  44784  fmtnoge3  44870  fmtnodvds  44884  odz2prm2pw  44903  fmtnole4prm  44918  lighneallem4b  44949  mogoldbb  45125  nnsum4primesevenALTV  45141  bgoldbtbndlem3  45147  ringrng  45325  isringrng  45327  lidlrng  45373  ssnn0ssfz  45573  lmod1  45721  elfzolborelfzop1  45748  nnolog2flm1  45824