Theorem syl3anbrc 1344

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 234	1 ⊢ (𝜑 → 𝜏)

Syntax hints:   → wi 4   ↔ wb 206   ∧ w3a 1086

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

This theorem is referenced by:  soisores  7261  limuni3  7782  onfununi  8261  smores2  8274  smoiso  8282  oelimcl  8515  iserd  8648  resixp  8857  undifixp  8858  alephval3  9998  canthwelem  10538  canthwe  10539  r1limwun  10624  wunex2  10626  tskcard  10669  gruina  10706  eluzmn  12736  eluzuzle  12738  uztrn  12747  eluzadd  12758  eluzsub  12759  subeluzsub  12766  nn0pzuz  12800  zsupss  12832  nn0ge2m1nnALT  12837  xov1plusxeqvd  13395  ige2m1fz  13514  0elfz  13521  uzsubfz0  13533  elfzmlbm  13535  difelfzle  13538  difelfznle  13539  fvffz0  13543  elfzolt2b  13567  elfzolt3b  13568  elfzouz2  13571  fzossrbm1  13585  elfzo0  13597  eluzgtdifelfzo  13624  elfzodifsumelfzo  13628  fzonn0p1  13639  fzonn0p1p1  13641  fzo0sn0fzo1  13652  ssfzo12bi  13658  fzoopth  13659  ubmelm1fzo  13660  elfzonelfzo  13666  fzosplitprm1  13675  fzostep1  13683  fvinim0ffz  13686  flword2  13714  uzsup  13764  modfzo0difsn  13847  modsumfzodifsn  13848  fsuppmapnn0fiub  13895  suppssfz  13898  1elfz0hash  14294  fzsdom2  14332  ccatdmss  14486  ccatrn  14494  ccat2s1fvw  14543  pfxn0  14591  pfxtrcfv0  14598  pfxtrcfvl  14601  swrdswrd  14609  swrdccatin1  14629  pfxccat3  14638  pfxccat3a  14642  repswswrd  14688  cshwidxmod  14707  cshw1  14726  cshwcsh2id  14732  swrds2  14844  pfx2  14851  2swrd2eqwrdeq  14857  ccat2s1fvwALT  14859  rexuzre  15257  limsupgre  15385  rlimclim1  15449  rlimclim  15450  climrlim2  15451  isercolllem1  15569  isercoll  15572  climcndslem1  15753  fallfacval4  15947  tanhbnd  16067  sinbnd2  16088  cosbnd2  16089  rpnnen2lem12  16131  nn0o  16291  bitsfzolem  16342  bitsfzo  16343  bitsmod  16344  bitsfi  16345  bitsinv1lem  16349  bitsinv1  16350  smueqlem  16398  dvdsnprmd  16598  2mulprm  16601  hashgcdlem  16696  prm23lt5  16723  zgz  16842  gznegcl  16844  gzcjcl  16845  gzaddcl  16846  gzmulcl  16847  vdwlem9  16898  prmgaplem3  16962  prmgaplem4  16963  cshwshashlem2  17005  setsstruct2  17082  ismred  17501  isfuncd  17769  homdmcoa  17971  isdrs2  18209  fpwipodrs  18443  ipodrsima  18444  chnub  18525  chnso  18527  sgrp2rid2ex  18832  subgid  19038  issubg2  19051  subsubg  19059  gaorber  19218  orbsta  19223  pmtrfconj  19376  psgnunilem2  19405  psgnunilem3  19406  psgnunilem4  19407  pgpfi1  19505  subgpgp  19507  pgpssslw  19524  subgslw  19526  sylow2alem2  19528  fislw  19535  sylow3lem3  19539  efgs1  19645  efgsp1  19647  efgsres  19648  efgredleme  19653  efgcpbllemb  19665  lt6abl  19805  telgsumfzs  19899  ablfac1eu  19985  submomnd  20042  isrngd  20089  prdsrngd  20092  ringrng  20201  isringrng  20203  isringd  20207  ringsrg  20213  ring1  20226  prdsringd  20237  subrngid  20462  subrngsubg  20465  issubrng2  20471  subsubrng  20476  subrgsubg  20490  subrgsubrng  20491  sdrgid  20705  cntzsdrg  20715  subdrgint  20716  sdrgint  20717  suborng  20789  islmodd  20797  islssd  20866  islss4  20893  dflidl2rng  21153  rnglidl0  21164  rnglidl1  21167  rnglidlrng  21182  rng2idlsubrng  21200  rhmpreimaidl  21212  gzrngunit  21368  expmhm  21371  zringunit  21401  prmirredlem  21407  znidomb  21496  isphld  21589  ocvocv  21606  ocvlss  21607  frlmlbs  21732  psdmul  22079  gsummoncoe1  22221  mp2pm2mplem4  22722  chfacfisf  22767  chfacfisfcpmat  22768  chfacfscmulfsupp  22772  chfacfpmmulfsupp  22776  chfacfpmmulgsum2  22778  2ndcctbss  23368  finlocfin  23433  dissnlocfin  23442  locfindis  23443  locfincf  23444  isfild  23771  infil  23776  neifil  23793  flimfcls  23939  istgp2  24004  oppgtmd  24010  oppgtgp  24011  distgp  24012  indistgp  24013  efmndtmd  24014  submtmd  24017  subgtgp  24018  symgtgp  24019  qustgplem  24034  prdstmdd  24037  prdstgpd  24038  tlmtgp  24109  isngp4  24525  subgngp  24548  ngptgp  24549  tngngp2  24565  nrgtrg  24603  nrgtdrg  24606  elii2  24857  icopnfcnv  24865  xrhmeo  24869  lebnumii  24890  phtpcer  24919  reparpht  24923  phtpcco2  24924  pcohtpy  24945  pcoass  24949  pcorevlem  24951  isclmi  25002  isncvsngpd  25075  cphsubrglem  25102  cphclm  25114  phclm  25157  tcphcph  25162  clsocv  25175  cphsscph  25176  cmslssbn  25297  pjthlem2  25363  ovolf  25408  iundisj2  25475  vitalilem2  25535  vitali  25539  itg2monolem3  25678  dvfsumlem1  25957  dvfsumlem3  25960  mon1puc1p  26081  uc1pmon1p  26082  mon1pid  26084  ply1remlem  26095  drnguc1p  26104  plyaddlem1  26143  coeidlem  26167  aannenlem2  26262  radcnvcl  26351  pilem2  26387  coseq00topi  26436  coseq0negpitopi  26437  tangtx  26439  tanabsge  26440  cosq14gt0  26444  cosq14ge0  26445  cosq34lt1  26461  cosordlem  26464  cos0pilt1  26466  sinord  26468  resinf1o  26470  tanord1  26471  tanord  26472  efif1olem3  26478  efsubm  26485  relogrn  26495  logimclad  26506  logrnaddcl  26508  logneg  26522  logcj  26540  argregt0  26544  argrege0  26545  argimgt0  26546  argimlt0  26547  logimul  26548  logneg2  26549  logdmnrp  26575  logcnlem4  26579  dvloglem  26582  logf1o2  26584  efopnlem2  26591  cxpsqrtlem  26636  relogbval  26707  nnlogbexp  26716  relogbcxp  26720  relogbcxpb  26722  logbgt0b  26728  asinneg  26821  asinsin  26827  acoscos  26828  acosbnd  26835  atancj  26845  atanlogaddlem  26848  atanlogsublem  26850  atanlogsub  26851  atantan  26858  atanbndlem  26860  atans2  26866  leibpi  26877  scvxcvx  26921  jensenlem2  26923  emcllem7  26937  basellem1  27016  ppisval  27039  chtdif  27093  ppidif  27098  ppiub  27140  chtublem  27147  chtub  27148  lgsdilem2  27269  gausslemma2dlem1a  27301  gausslemma2dlem2  27303  gausslemma2dlem5  27307  gausslemma2dlem6  27308  lgsquadlem1  27316  lgsquadlem2  27317  lgsquadlem3  27318  2lgslem1  27330  2sqlem3  27356  chebbnd1lem1  27405  chebbnd1lem2  27406  chebbnd1lem3  27407  dchrisumlem2  27426  dchrvmasumlem2  27434  dchrvmasumiflem1  27437  dchrisum0flblem2  27445  mulog2sumlem2  27471  logdivbnd  27492  pntpbnd2  27523  pntibndlem1  27525  pntibnd  27529  pntlemc  27531  pntlemg  27534  pntlemq  27537  pntlemf  27541  padicabvf  27567  padicabvcxp  27568  ostth2  27573  noextend  27603  noextendseq  27604  nosupno  27640  noinfno  27655  ttgcontlem1  28861  axpaschlem  28916  nbgr2vtx1edg  29326  nbuhgr2vtx1edgb  29328  cusgrexi  29419  structtocusgr  29422  pthdadjvtx  29704  pthdlem1  29742  pthd  29745  crctcshwlkn0lem3  29788  crctcshwlkn0lem4  29789  crctcshwlkn0lem5  29790  crctcshwlkn0lem7  29792  wlkiswwlks1  29843  wwlksm1edg  29857  wwlksnred  29868  wwlksnredwwlkn  29871  wwlksnextproplem3  29887  clwlkclwwlklem2fv1  29970  clwlkclwwlklem2fv2  29971  clwlkclwwlklem2a  29973  clwlkclwwlklem2  29975  clwwisshclwwslemlem  29988  clwwisshclwwslem  29989  erclwwlkref  29995  clwwlkel  30021  clwwlkf  30022  wwlksext2clwwlk  30032  wwlksubclwwlk  30033  umgr2cwwkdifex  30040  1pthd  30118  eucrctshift  30218  dlwwlknondlwlknonf1olem1  30339  numclwlk2lem2f  30352  frgrreggt1  30368  grpoinvf  30507  strlem3a  32227  hstrlem3a  32235  iundisj2f  32565  fcoinver  32579  fresf1o  32608  ssnnssfz  32765  bcm1n  32772  iundisj2fi  32774  fsumrp0cl  32997  cycpmco2lem6  33095  fxpsdrg  33139  lmodslmd  33168  fldgensdrg  33275  intlidl  33380  idlinsubrg  33391  rhmimaidl  33392  ssdifidllem  33416  ssmxidllem  33433  1arithidomlem1  33495  1arithidomlem2  33496  1arithidom  33497  fldextsdrg  33662  fldextrspunlem2  33685  fldextrspundgdvdslem  33688  fldextrspundgdvds  33689  minplyirred  33719  algextdeglem4  33728  algextdeglem8  33732  rtelextdg2lem  33734  constrsdrg  33783  2sqr3minply  33788  cos9thpiminply  33796  locfinreflem  33848  locfinref  33849  xrge0iifcnv  33941  xrge0iifiso  33943  xrge0iifhom  33945  esumc  34059  esumle  34066  esumlef  34070  esumpinfsum  34085  esumpcvgval  34086  fiunelros  34182  voliune  34237  volfiniune  34238  sibfinima  34347  eulerpartlemt  34379  fiblem  34406  fibp1  34409  dstrvprob  34480  ballotlemsel1i  34521  ballotlemfrceq  34537  plymulx0  34555  signstfvc  34582  signstfveq0  34585  bnj944  34945  bnj998  34964  bnj1136  35004  bnj1408  35043  erdszelem4  35226  erdszelem8  35230  txsconnlem  35272  cvxsconn  35275  cvmliftpht  35350  snmlff  35361  elmrsubrn  35552  msrf  35574  mthmpps  35614  sinccvglem  35704  trer  36349  poimirlem6  37665  poimirlem7  37666  poimirlem9  37668  poimirlem17  37676  poimirlem20  37679  poimirlem28  37687  poimirlem29  37688  poimirlem30  37689  poimirlem31  37690  poimirlem32  37691  areacirc  37752  nnubfi  37789  prter1  38917  lkrlss  39133  diaf11N  41087  dibf11N  41199  lclkr  41571  lclkrs  41577  lcfrlem9  41588  lcfr  41623  mapd1o  41686  hdmapf1oN  41903  hgmapf1oN  41941  frlmvscadiccat  42538  fimgmcyc  42566  nacsfix  42744  eldioph2lem1  42792  irrapxlem1  42854  rmxypairf1o  42943  jm2.27a  43037  hbtlem2  43156  hbt  43162  mon1psubm  43231  onnog  43461  pren2d  43588  binomcxplemnotnn0  44388  elixpconstg  45125  elfzfzo  45317  monoords  45337  elfzod  45437  eluzd  45446  fmul01lt1lem2  45624  sumnnodd  45669  ioodvbdlimc1lem2  45969  ioodvbdlimc2lem  45971  iblsplit  46003  iblspltprt  46010  itgspltprt  46016  stoweidlem11  46048  stoweidlem17  46054  fourierdlem12  46156  fourierdlem20  46164  fourierdlem25  46169  fourierdlem37  46181  fourierdlem41  46185  fourierdlem48  46191  fourierdlem49  46192  fourierdlem50  46193  fourierdlem54  46197  fourierdlem64  46207  fourierdlem73  46216  fourierdlem79  46222  fourierdlem102  46245  fourierdlem111  46254  fourierdlem114  46257  etransclem23  46294  etransclem48  46319  ormkglobd  46912  2elfz2melfz  47348  elfzlble  47350  ceilhalfelfzo1  47360  1elfzo1ceilhalf1  47367  difltmodne  47372  modm2nep1  47396  modm1nep2  47398  modm1p1ne  47400  iccpartiltu  47452  iccpartigtl  47453  iccpartlt  47454  iccpartgt  47457  lswn0  47474  fmtnoge3  47560  fmtnodvds  47574  odz2prm2pw  47593  fmtnole4prm  47608  lighneallem4b  47639  mogoldbb  47815  nnsum4primesevenALTV  47831  bgoldbtbndlem3  47837  gpgprismgriedgdmss  48082  gpgprismgrusgra  48088  gpg3nbgrvtx0  48106  gpg3nbgrvtx0ALT  48107  gpg5nbgrvtx03star  48110  gpg5nbgr3star  48111  gpg3kgrtriexlem3  48115  gpg3kgrtriexlem4  48116  gpg3kgrtriexlem6  48118  gpgprismgr4cycllem3  48127  gpgprismgr4cycllem9  48133  ssnn0ssfz  48379  lmod1  48523  elfzolborelfzop1  48550  nnolog2flm1  48621  funcf2lem2  49113  isnatd  49254