Theorem syl3anbrc 1362

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  soisores  7327  limuni3  7849  onfununi  8329  smores2  8342  smoiso  8350  oelimcl  8587  iserd  8722  resixp  8932  undifixp  8933  alephval3  10095  canthwelem  10636  canthwe  10637  r1limwun  10722  wunex2  10724  tskcard  10767  gruina  10804  eluzmn  12870  eluzuzle  12872  uztrn  12881  eluzadd  12892  eluzsub  12893  subeluzsub  12896  nn0pzuz  12930  zsupss  12962  nn0ge2m1nnALT  12967  xov1plusxeqvd  13526  ige2m1fz  13647  0elfz  13654  uzsubfz0  13666  elfzmlbm  13668  difelfzle  13671  difelfznle  13672  fvffz0  13676  elfzod  13693  elfzolt2b  13701  elfzolt3b  13702  elfzouz2  13705  fzossrbm1  13719  elfzo0  13731  eluzgtdifelfzo  13758  elfzodifsumelfzo  13762  fzonn0p1  13773  fzonn0p1p1  13775  fzo0sn0fzo1  13786  ssfzo12bi  13792  fzoopth  13793  ubmelm1fzo  13794  elfzonelfzo  13800  fzosplitprm1  13809  fzostep1  13817  fvinim0ffz  13820  flword2  13848  uzsup  13898  modfzo0difsn  13981  modsumfzodifsn  13982  fsuppmapnn0fiub  14029  suppssfz  14032  1elfz0hash  14428  fzsdom2  14467  ccatdmss  14621  ccatrn  14629  ccat2s1fvw  14678  pfxn0  14726  pfxtrcfv0  14733  pfxtrcfvl  14736  swrdswrd  14744  swrdccatin1  14764  pfxccat3  14773  pfxccat3a  14777  repswswrd  14823  cshwidxmod  14842  cshw1  14861  cshwcsh2id  14867  swrds2  14979  pfx2  14986  2swrd2eqwrdeq  14992  ccat2s1fvwALT  14994  rexuzre  15406  limsupgre  15534  rlimclim1  15598  rlimclim  15599  climrlim2  15600  isercolllem1  15718  isercoll  15721  climcndslem1  15905  fallfacval4  16098  tanhbnd  16218  sinbnd2  16239  cosbnd2  16240  rpnnen2lem12  16282  nn0o  16442  bitsfzolem  16493  bitsfzo  16494  bitsmod  16495  bitsfi  16496  bitsinv1lem  16500  bitsinv1  16501  smueqlem  16549  dvdsnprmd  16749  2mulprm  16752  hashgcdlem  16848  prm23lt5  16875  zgz  16994  gznegcl  16996  gzcjcl  16997  gzaddcl  16998  gzmulcl  16999  vdwlem9  17050  prmgaplem3  17114  prmgaplem4  17115  cshwshashlem2  17157  setsstruct2  17235  ismred  17655  isfuncd  17923  homdmcoa  18125  isdrs2  18363  fpwipodrs  18597  ipodrsima  18598  chnub  18679  chnso  18681  sgrp2rid2ex  18990  subgid  19195  issubg2  19209  subsubg  19217  gaorber  19379  orbsta  19384  pmtrfconj  19537  psgnunilem2  19566  psgnunilem3  19567  psgnunilem4  19568  pgpfi1  19666  subgpgp  19668  pgpssslw  19685  subgslw  19687  sylow2alem2  19689  fislw  19696  sylow3lem3  19700  efgs1  19806  efgsp1  19808  efgsres  19809  efgredleme  19814  efgcpbllemb  19826  lt6abl  19966  telgsumfzs  20060  ablfac1eu  20146  submomnd  20203  isrngd  20252  prdsrngd  20255  ringrng  20369  isringrng  20371  isringd  20375  ringsrg  20381  ring1  20394  prdsringd  20403  subrngid  20635  subrngsubg  20638  issubrng2  20644  subsubrng  20649  subrgsubg  20663  subrgsubrng  20664  sdrgid  20876  cntzsdrg  20886  subdrgint  20887  sdrgint  20888  suborng  20960  islmodd  20968  islssd  21037  islss4  21064  dflidl2rng  21324  rnglidl0  21336  rnglidl1  21339  unichnlidl  21343  rnglidlrng  21362  rng2idlsubrng  21385  rhmpreimaidl  21397  ssdifidllem  21465  gzrngunit  21564  expmhm  21567  zringunit  21597  prmirredlem  21603  znidomb  21692  isphld  21785  ocvocv  21802  ocvlss  21803  frlmlbs  21928  psdmul  22310  gsummoncoe1  22449  mp2pm2mplem4  22947  chfacfisf  22992  chfacfisfcpmat  22993  chfacfscmulfsupp  22997  chfacfpmmulfsupp  23001  chfacfpmmulgsum2  23003  2ndcctbss  23593  finlocfin  23658  dissnlocfin  23667  locfindis  23668  locfincf  23669  isfild  23996  infil  24001  neifil  24018  flimfcls  24164  istgp2  24229  oppgtmd  24235  oppgtgp  24236  distgp  24237  indistgp  24238  efmndtmd  24239  submtmd  24242  subgtgp  24243  symgtgp  24244  qustgplem  24259  prdstmdd  24262  prdstgpd  24263  tlmtgp  24334  isngp4  24750  subgngp  24773  ngptgp  24774  tngngp2  24790  nrgtrg  24828  nrgtdrg  24831  elii2  25076  icopnfcnv  25082  xrhmeo  25086  lebnumii  25106  phtpcer  25135  reparpht  25138  phtpcco2  25139  pcohtpy  25160  pcoass  25164  pcorevlem  25166  isclmi  25217  isncvsngpd  25290  cphsubrglem  25317  cphclm  25329  phclm  25372  tcphcph  25377  clsocv  25390  cphsscph  25391  cmslssbn  25512  pjthlem2  25578  ovolf  25622  iundisj2  25689  vitalilem2  25749  vitali  25753  itg2monolem3  25892  dvfsumlem1  26166  dvfsumlem3  26168  mon1puc1p  26289  uc1pmon1p  26290  mon1pid  26292  ply1remlem  26303  drnguc1p  26312  plyaddlem1  26351  coeidlem  26375  plyn0mulidp  26423  aannenlem2  26473  radcnvcl  26561  pilem2  26596  coseq00topi  26648  coseq0negpitopi  26649  tangtx  26651  tanabsge  26652  cosq14gt0  26656  cosq14ge0  26657  cosq34lt1  26673  cosordlem  26676  cos0pilt1  26678  sinord  26680  resinf1o  26682  tanord1  26683  tanord  26684  efif1olem3  26690  efsubm  26697  relogrn  26707  logimclad  26718  logrnaddcl  26720  logneg  26734  logcj  26752  argregt0  26756  argrege0  26757  argimgt0  26758  argimlt0  26759  logimul  26760  logneg2  26761  logdmnrp  26787  logcnlem4  26791  dvloglem  26794  logf1o2  26796  efopnlem2  26803  cxpsqrtlem  26848  relogbval  26918  nnlogbexp  26927  relogbcxp  26931  relogbcxpb  26933  logbgt0b  26939  asinneg  27032  asinsin  27038  acoscos  27039  acosbnd  27046  atancj  27056  atanlogaddlem  27059  atanlogsublem  27061  atanlogsub  27062  atantan  27069  atanbndlem  27071  atans2  27077  leibpi  27088  scvxcvx  27131  jensenlem2  27133  emcllem7  27147  basellem1  27226  ppisval  27249  chtdif  27303  ppidif  27308  ppiub  27349  chtublem  27356  chtub  27357  lgsdilem2  27478  gausslemma2dlem1a  27510  gausslemma2dlem2  27512  gausslemma2dlem5  27516  gausslemma2dlem6  27517  lgsquadlem1  27525  lgsquadlem2  27526  lgsquadlem3  27527  2lgslem1  27539  2sqlem3  27565  chebbnd1lem1  27614  chebbnd1lem2  27615  chebbnd1lem3  27616  dchrisumlem2  27635  dchrvmasumlem2  27643  dchrvmasumiflem1  27646  dchrisum0flblem2  27654  mulog2sumlem2  27680  logdivbnd  27701  pntpbnd2  27732  pntibndlem1  27734  pntibnd  27738  pntlemc  27740  pntlemg  27743  pntlemq  27746  pntlemf  27750  padicabvf  27776  padicabvcxp  27777  ostth2  27782  noextend  27811  noextendseq  27812  nosupno  27848  noinfno  27863  ttgcontlem1  29215  axpaschlem  29271  nbgr2vtx1edg  29681  nbuhgr2vtx1edgb  29683  cusgrexi  29774  structtocusgr  29777  pthdadjvtx  30058  pthdlem1  30096  pthd  30099  crctcshwlkn0lem3  30142  crctcshwlkn0lem4  30143  crctcshwlkn0lem5  30144  crctcshwlkn0lem7  30146  wlkiswwlks1  30197  wwlksm1edg  30211  wwlksnred  30222  wwlksnredwwlkn  30225  wwlksnextproplem3  30241  clwlkclwwlklem2fv1  30327  clwlkclwwlklem2fv2  30328  clwlkclwwlklem2a  30330  clwlkclwwlklem2  30332  clwwisshclwwslemlem  30345  clwwisshclwwslem  30346  erclwwlkref  30352  clwwlkel  30378  clwwlkf  30379  wwlksext2clwwlk  30389  wwlksubclwwlk  30390  umgr2cwwkdifex  30397  1pthd  30475  eucrctshift  30575  dlwwlknondlwlknonf1olem1  30696  numclwlk2lem2f  30709  frgrreggt1  30725  grpoinvf  30865  strlem3a  32585  hstrlem3a  32593  iundisj2f  32916  fcoinver  32930  fresf1o  32957  ssnnssfz  33113  bcm1n  33121  iundisj2fi  33123  fsumrp0cl  33322  cycpmco2lem6  33432  fxpsdrg  33476  lmodslmd  33505  fldgensdrg  33616  intlidl  33709  idlinsubrg  33720  rhmimaidl  33721  ssmxidllem  33737  dflringlem2  33766  1arithidomlem1  33806  1arithidomlem2  33807  1arithidom  33808  fldextsdrg  34025  fldextrspunlem2  34048  fldextrspundgdvdslem  34051  fldextrspundgdvds  34052  minplyirred  34082  algextdeglem4  34091  algextdeglem8  34095  rtelextdg2lem  34097  constrsdrg  34146  2sqr3minply  34151  cos9thpiminply  34159  locfinreflem  34211  locfinref  34212  xrge0iifcnv  34304  xrge0iifiso  34306  xrge0iifhom  34308  esumc  34422  esumle  34429  esumlef  34433  esumpinfsum  34448  esumpcvgval  34449  fiunelros  34545  voliune  34600  volfiniune  34601  sibfinima  34710  eulerpartlemt  34742  fiblem  34769  fibp1  34772  dstrvprob  34843  ballotlemsel1i  34884  ballotlemfrceq  34900  signstfvc  34942  signstfveq0  34945  bnj944  35307  bnj998  35326  bnj1136  35366  bnj1408  35405  erdszelem4  35667  erdszelem8  35671  txsconnlem  35713  cvxsconn  35716  cvmliftpht  35791  snmlff  35802  elmrsubrn  35993  msrf  36015  mthmpps  36055  sinccvglem  36145  trer  36808  poimirlem6  38258  poimirlem7  38259  poimirlem9  38261  poimirlem17  38269  poimirlem20  38272  poimirlem28  38280  poimirlem29  38281  poimirlem30  38282  poimirlem31  38283  poimirlem32  38284  areacirc  38345  nnubfi  38382  prter1  39634  lkrlss  39850  diaf11N  41804  dibf11N  41916  lclkr  42288  lclkrs  42294  lcfrlem9  42305  lcfr  42340  mapd1o  42403  hdmapf1oN  42620  hgmapf1oN  42658  frlmvscadiccat  43261  fimgmcyc  43285  nacsfix  43426  eldioph2lem1  43474  irrapxlem1  43532  rmxypairf1o  43621  jm2.27a  43715  hbtlem2  43834  hbt  43840  mon1psubm  43909  onnoxpg  44138  pren2d  44265  binomcxplemnotnn0  45049  elixpconstg  45790  elfzfzo  45979  monoords  45999  eluzd  46106  fmul01lt1lem2  46284  sumnnodd  46329  ioodvbdlimc1lem2  46629  ioodvbdlimc2lem  46631  iblsplit  46663  iblspltprt  46670  itgspltprt  46676  stoweidlem11  46708  stoweidlem17  46714  fourierdlem12  46816  fourierdlem20  46824  fourierdlem25  46829  fourierdlem37  46841  fourierdlem41  46845  fourierdlem48  46851  fourierdlem50  46853  fourierdlem54  46857  fourierdlem64  46867  fourierdlem73  46876  fourierdlem79  46882  fourierdlem102  46905  fourierdlem111  46914  fourierdlem114  46917  etransclem23  46954  etransclem48  46979  ormkglobd  47574  chnsubseq  47579  2elfz2melfz  48038  elfzlble  48040  ceilhalfelfzo1  48054  1elfzo1ceilhalf1  48061  difltmodne  48068  modm2nep1  48092  modm1nep2  48094  modm1p1ne  48096  iccpartiltu  48154  iccpartigtl  48155  iccpartlt  48156  iccpartgt  48159  lswn0  48176  fmtnoge3  48265  fmtnodvds  48279  odz2prm2pw  48298  fmtnole4prm  48313  lighneallem4b  48344  nprmdvdsfacm1lem3  48357  nprmdvdsfacm1lem4  48358  nprmdvdsfacm1  48359  mogoldbb  48533  nnsum4primesevenALTV  48549  bgoldbtbndlem3  48555  gpgprismgriedgdmss  48800  gpgprismgrusgra  48806  gpg3nbgrvtx0  48824  gpg3nbgrvtx0ALT  48825  gpg5nbgrvtx03star  48828  gpg5nbgr3star  48829  gpg3kgrtriexlem3  48833  gpg3kgrtriexlem4  48834  gpg3kgrtriexlem6  48836  gpgprismgr4cycllem3  48845  gpgprismgr4cycllem9  48851  ssnn0ssfz  49112  lmod1  49255  elfzolborelfzop1  49282  nnolog2flm1  49353  funcf2lem2  49843  isnatd  49984