Theorem syl3anbrc 1360

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

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

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 1103

This theorem is referenced by:  soisores  7315  limuni3  7836  onfununi  8316  smores2  8329  smoiso  8337  oelimcl  8574  iserd  8709  resixp  8919  undifixp  8920  alephval3  10082  canthwelem  10623  canthwe  10624  r1limwun  10709  wunex2  10711  tskcard  10754  gruina  10791  eluzmn  12857  eluzuzle  12859  uztrn  12868  eluzadd  12879  eluzsub  12880  subeluzsub  12883  nn0pzuz  12917  zsupss  12949  nn0ge2m1nnALT  12954  xov1plusxeqvd  13513  ige2m1fz  13633  0elfz  13640  uzsubfz0  13652  elfzmlbm  13654  difelfzle  13657  difelfznle  13658  fvffz0  13662  elfzod  13679  elfzolt2b  13687  elfzolt3b  13688  elfzouz2  13691  fzossrbm1  13705  elfzo0  13717  eluzgtdifelfzo  13744  elfzodifsumelfzo  13748  fzonn0p1  13759  fzonn0p1p1  13761  fzo0sn0fzo1  13772  ssfzo12bi  13778  fzoopth  13779  ubmelm1fzo  13780  elfzonelfzo  13786  fzosplitprm1  13795  fzostep1  13803  fvinim0ffz  13806  flword2  13834  uzsup  13884  modfzo0difsn  13967  modsumfzodifsn  13968  fsuppmapnn0fiub  14015  suppssfz  14018  1elfz0hash  14414  fzsdom2  14453  ccatdmss  14607  ccatrn  14615  ccat2s1fvw  14664  pfxn0  14712  pfxtrcfv0  14719  pfxtrcfvl  14722  swrdswrd  14730  swrdccatin1  14750  pfxccat3  14759  pfxccat3a  14763  repswswrd  14809  cshwidxmod  14828  cshw1  14847  cshwcsh2id  14853  swrds2  14965  pfx2  14972  2swrd2eqwrdeq  14978  ccat2s1fvwALT  14980  rexuzre  15392  limsupgre  15520  rlimclim1  15584  rlimclim  15585  climrlim2  15586  isercolllem1  15704  isercoll  15707  climcndslem1  15891  fallfacval4  16085  tanhbnd  16205  sinbnd2  16226  cosbnd2  16227  rpnnen2lem12  16269  nn0o  16429  bitsfzolem  16480  bitsfzo  16481  bitsmod  16482  bitsfi  16483  bitsinv1lem  16487  bitsinv1  16488  smueqlem  16536  dvdsnprmd  16736  2mulprm  16739  hashgcdlem  16835  prm23lt5  16862  zgz  16981  gznegcl  16983  gzcjcl  16984  gzaddcl  16985  gzmulcl  16986  vdwlem9  17037  prmgaplem3  17101  prmgaplem4  17102  cshwshashlem2  17144  setsstruct2  17222  ismred  17642  isfuncd  17910  homdmcoa  18112  isdrs2  18350  fpwipodrs  18584  ipodrsima  18585  chnub  18666  chnso  18668  sgrp2rid2ex  18977  subgid  19182  issubg2  19196  subsubg  19204  gaorber  19366  orbsta  19371  pmtrfconj  19524  psgnunilem2  19553  psgnunilem3  19554  psgnunilem4  19555  pgpfi1  19653  subgpgp  19655  pgpssslw  19672  subgslw  19674  sylow2alem2  19676  fislw  19683  sylow3lem3  19687  efgs1  19793  efgsp1  19795  efgsres  19796  efgredleme  19801  efgcpbllemb  19813  lt6abl  19953  telgsumfzs  20047  ablfac1eu  20133  submomnd  20190  isrngd  20239  prdsrngd  20242  ringrng  20356  isringrng  20358  isringd  20362  ringsrg  20368  ring1  20381  prdsringd  20390  subrngid  20622  subrngsubg  20625  issubrng2  20631  subsubrng  20636  subrgsubg  20650  subrgsubrng  20651  sdrgid  20861  cntzsdrg  20871  subdrgint  20872  sdrgint  20873  suborng  20945  islmodd  20953  islssd  21022  islss4  21049  dflidl2rng  21309  rnglidl0  21321  rnglidl1  21324  unichnlidl  21328  rnglidlrng  21343  rng2idlsubrng  21363  rhmpreimaidl  21375  ssdifidllem  21441  gzrngunit  21540  expmhm  21543  zringunit  21573  prmirredlem  21579  znidomb  21668  isphld  21761  ocvocv  21778  ocvlss  21779  frlmlbs  21904  psdmul  22286  gsummoncoe1  22425  mp2pm2mplem4  22923  chfacfisf  22968  chfacfisfcpmat  22969  chfacfscmulfsupp  22973  chfacfpmmulfsupp  22977  chfacfpmmulgsum2  22979  2ndcctbss  23569  finlocfin  23634  dissnlocfin  23643  locfindis  23644  locfincf  23645  isfild  23972  infil  23977  neifil  23994  flimfcls  24140  istgp2  24205  oppgtmd  24211  oppgtgp  24212  distgp  24213  indistgp  24214  efmndtmd  24215  submtmd  24218  subgtgp  24219  symgtgp  24220  qustgplem  24235  prdstmdd  24238  prdstgpd  24239  tlmtgp  24310  isngp4  24726  subgngp  24749  ngptgp  24750  tngngp2  24766  nrgtrg  24804  nrgtdrg  24807  elii2  25052  icopnfcnv  25058  xrhmeo  25062  lebnumii  25082  phtpcer  25111  reparpht  25114  phtpcco2  25115  pcohtpy  25136  pcoass  25140  pcorevlem  25142  isclmi  25193  isncvsngpd  25266  cphsubrglem  25293  cphclm  25305  phclm  25348  tcphcph  25353  clsocv  25366  cphsscph  25367  cmslssbn  25488  pjthlem2  25554  ovolf  25598  iundisj2  25665  vitalilem2  25725  vitali  25729  itg2monolem3  25868  dvfsumlem1  26142  dvfsumlem3  26144  mon1puc1p  26265  uc1pmon1p  26266  mon1pid  26268  ply1remlem  26279  drnguc1p  26288  plyaddlem1  26327  coeidlem  26351  plyn0mulidp  26399  aannenlem2  26447  radcnvcl  26534  pilem2  26569  coseq00topi  26621  coseq0negpitopi  26622  tangtx  26624  tanabsge  26625  cosq14gt0  26629  cosq14ge0  26630  cosq34lt1  26646  cosordlem  26649  cos0pilt1  26651  sinord  26653  resinf1o  26655  tanord1  26656  tanord  26657  efif1olem3  26663  efsubm  26670  relogrn  26680  logimclad  26691  logrnaddcl  26693  logneg  26707  logcj  26725  argregt0  26729  argrege0  26730  argimgt0  26731  argimlt0  26732  logimul  26733  logneg2  26734  logdmnrp  26760  logcnlem4  26764  dvloglem  26767  logf1o2  26769  efopnlem2  26776  cxpsqrtlem  26821  relogbval  26891  nnlogbexp  26900  relogbcxp  26904  relogbcxpb  26906  logbgt0b  26912  asinneg  27005  asinsin  27011  acoscos  27012  acosbnd  27019  atancj  27029  atanlogaddlem  27032  atanlogsublem  27034  atanlogsub  27035  atantan  27042  atanbndlem  27044  atans2  27050  leibpi  27061  scvxcvx  27104  jensenlem2  27106  emcllem7  27120  basellem1  27199  ppisval  27222  chtdif  27276  ppidif  27281  ppiub  27322  chtublem  27329  chtub  27330  lgsdilem2  27451  gausslemma2dlem1a  27483  gausslemma2dlem2  27485  gausslemma2dlem5  27489  gausslemma2dlem6  27490  lgsquadlem1  27498  lgsquadlem2  27499  lgsquadlem3  27500  2lgslem1  27512  2sqlem3  27538  chebbnd1lem1  27587  chebbnd1lem2  27588  chebbnd1lem3  27589  dchrisumlem2  27608  dchrvmasumlem2  27616  dchrvmasumiflem1  27619  dchrisum0flblem2  27627  mulog2sumlem2  27653  logdivbnd  27674  pntpbnd2  27705  pntibndlem1  27707  pntibnd  27711  pntlemc  27713  pntlemg  27716  pntlemq  27719  pntlemf  27723  padicabvf  27749  padicabvcxp  27750  ostth2  27755  noextend  27784  noextendseq  27785  nosupno  27821  noinfno  27836  ttgcontlem1  29139  axpaschlem  29195  nbgr2vtx1edg  29605  nbuhgr2vtx1edgb  29607  cusgrexi  29698  structtocusgr  29701  pthdadjvtx  29982  pthdlem1  30020  pthd  30023  crctcshwlkn0lem3  30066  crctcshwlkn0lem4  30067  crctcshwlkn0lem5  30068  crctcshwlkn0lem7  30070  wlkiswwlks1  30121  wwlksm1edg  30135  wwlksnred  30146  wwlksnredwwlkn  30149  wwlksnextproplem3  30165  clwlkclwwlklem2fv1  30251  clwlkclwwlklem2fv2  30252  clwlkclwwlklem2a  30254  clwlkclwwlklem2  30256  clwwisshclwwslemlem  30269  clwwisshclwwslem  30270  erclwwlkref  30276  clwwlkel  30302  clwwlkf  30303  wwlksext2clwwlk  30313  wwlksubclwwlk  30314  umgr2cwwkdifex  30321  1pthd  30399  eucrctshift  30499  dlwwlknondlwlknonf1olem1  30620  numclwlk2lem2f  30633  frgrreggt1  30649  grpoinvf  30789  strlem3a  32509  hstrlem3a  32517  iundisj2f  32841  fcoinver  32855  fresf1o  32884  ssnnssfz  33040  bcm1n  33048  iundisj2fi  33050  fsumrp0cl  33249  cycpmco2lem6  33359  fxpsdrg  33403  lmodslmd  33432  fldgensdrg  33545  intlidl  33639  idlinsubrg  33650  rhmimaidl  33651  ssmxidllem  33668  dflringlem2  33697  1arithidomlem1  33737  1arithidomlem2  33738  1arithidom  33739  fldextsdrg  33956  fldextrspunlem2  33979  fldextrspundgdvdslem  33982  fldextrspundgdvds  33983  minplyirred  34013  algextdeglem4  34022  algextdeglem8  34026  rtelextdg2lem  34028  constrsdrg  34077  2sqr3minply  34082  cos9thpiminply  34090  locfinreflem  34142  locfinref  34143  xrge0iifcnv  34235  xrge0iifiso  34237  xrge0iifhom  34239  esumc  34353  esumle  34360  esumlef  34364  esumpinfsum  34379  esumpcvgval  34380  fiunelros  34476  voliune  34531  volfiniune  34532  sibfinima  34641  eulerpartlemt  34673  fiblem  34700  fibp1  34703  dstrvprob  34774  ballotlemsel1i  34815  ballotlemfrceq  34831  signstfvc  34873  signstfveq0  34876  bnj944  35238  bnj998  35257  bnj1136  35297  bnj1408  35336  erdszelem4  35552  erdszelem8  35556  txsconnlem  35598  cvxsconn  35601  cvmliftpht  35676  snmlff  35687  elmrsubrn  35878  msrf  35900  mthmpps  35940  sinccvglem  36030  trer  36684  poimirlem6  38132  poimirlem7  38133  poimirlem9  38135  poimirlem17  38143  poimirlem20  38146  poimirlem28  38154  poimirlem29  38155  poimirlem30  38156  poimirlem31  38157  poimirlem32  38158  areacirc  38219  nnubfi  38256  prter1  39510  lkrlss  39726  diaf11N  41680  dibf11N  41792  lclkr  42164  lclkrs  42170  lcfrlem9  42181  lcfr  42216  mapd1o  42279  hdmapf1oN  42496  hgmapf1oN  42534  frlmvscadiccat  43135  fimgmcyc  43159  nacsfix  43300  eldioph2lem1  43348  irrapxlem1  43406  rmxypairf1o  43495  jm2.27a  43589  hbtlem2  43708  hbt  43714  mon1psubm  43783  onnoxpg  44012  pren2d  44139  binomcxplemnotnn0  44925  elixpconstg  45666  elfzfzo  45855  monoords  45875  eluzd  45982  fmul01lt1lem2  46160  sumnnodd  46205  ioodvbdlimc1lem2  46505  ioodvbdlimc2lem  46507  iblsplit  46539  iblspltprt  46546  itgspltprt  46552  stoweidlem11  46584  stoweidlem17  46590  fourierdlem12  46692  fourierdlem20  46700  fourierdlem25  46705  fourierdlem37  46717  fourierdlem41  46721  fourierdlem48  46727  fourierdlem50  46729  fourierdlem54  46733  fourierdlem64  46743  fourierdlem73  46752  fourierdlem79  46758  fourierdlem102  46781  fourierdlem111  46790  fourierdlem114  46793  etransclem23  46830  etransclem48  46855  ormkglobd  47450  chnsubseq  47455  2elfz2melfz  47911  elfzlble  47913  ceilhalfelfzo1  47927  1elfzo1ceilhalf1  47934  difltmodne  47941  modm2nep1  47965  modm1nep2  47967  modm1p1ne  47969  iccpartiltu  48027  iccpartigtl  48028  iccpartlt  48029  iccpartgt  48032  lswn0  48049  fmtnoge3  48138  fmtnodvds  48152  odz2prm2pw  48171  fmtnole4prm  48186  lighneallem4b  48217  nprmdvdsfacm1lem3  48230  nprmdvdsfacm1lem4  48231  nprmdvdsfacm1  48232  mogoldbb  48406  nnsum4primesevenALTV  48422  bgoldbtbndlem3  48428  gpgprismgriedgdmss  48673  gpgprismgrusgra  48679  gpg3nbgrvtx0  48697  gpg3nbgrvtx0ALT  48698  gpg5nbgrvtx03star  48701  gpg5nbgr3star  48702  gpg3kgrtriexlem3  48706  gpg3kgrtriexlem4  48707  gpg3kgrtriexlem6  48709  gpgprismgr4cycllem3  48718  gpgprismgr4cycllem9  48724  ssnn0ssfz  48981  lmod1  49124  elfzolborelfzop1  49151  nnolog2flm1  49222  funcf2lem2  49712  isnatd  49853