Theorem syl3anbrc 1345

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  soisores  7275  limuni3  7796  onfununi  8274  smores2  8287  smoiso  8295  oelimcl  8529  iserd  8663  resixp  8874  undifixp  8875  alephval3  10023  canthwelem  10564  canthwe  10565  r1limwun  10650  wunex2  10652  tskcard  10695  gruina  10732  eluzmn  12786  eluzuzle  12788  uztrn  12797  eluzadd  12808  eluzsub  12809  subeluzsub  12812  nn0pzuz  12846  zsupss  12878  nn0ge2m1nnALT  12883  xov1plusxeqvd  13442  ige2m1fz  13562  0elfz  13569  uzsubfz0  13581  elfzmlbm  13583  difelfzle  13586  difelfznle  13587  fvffz0  13591  elfzod  13608  elfzolt2b  13616  elfzolt3b  13617  elfzouz2  13620  fzossrbm1  13634  elfzo0  13646  eluzgtdifelfzo  13673  elfzodifsumelfzo  13677  fzonn0p1  13688  fzonn0p1p1  13690  fzo0sn0fzo1  13701  ssfzo12bi  13707  fzoopth  13708  ubmelm1fzo  13709  elfzonelfzo  13715  fzosplitprm1  13724  fzostep1  13732  fvinim0ffz  13735  flword2  13763  uzsup  13813  modfzo0difsn  13896  modsumfzodifsn  13897  fsuppmapnn0fiub  13944  suppssfz  13947  1elfz0hash  14343  fzsdom2  14381  ccatdmss  14535  ccatrn  14543  ccat2s1fvw  14592  pfxn0  14640  pfxtrcfv0  14647  pfxtrcfvl  14650  swrdswrd  14658  swrdccatin1  14678  pfxccat3  14687  pfxccat3a  14691  repswswrd  14737  cshwidxmod  14756  cshw1  14775  cshwcsh2id  14781  swrds2  14893  pfx2  14900  2swrd2eqwrdeq  14906  ccat2s1fvwALT  14908  rexuzre  15306  limsupgre  15434  rlimclim1  15498  rlimclim  15499  climrlim2  15500  isercolllem1  15618  isercoll  15621  climcndslem1  15805  fallfacval4  15999  tanhbnd  16119  sinbnd2  16140  cosbnd2  16141  rpnnen2lem12  16183  nn0o  16343  bitsfzolem  16394  bitsfzo  16395  bitsmod  16396  bitsfi  16397  bitsinv1lem  16401  bitsinv1  16402  smueqlem  16450  dvdsnprmd  16650  2mulprm  16653  hashgcdlem  16749  prm23lt5  16776  zgz  16895  gznegcl  16897  gzcjcl  16898  gzaddcl  16899  gzmulcl  16900  vdwlem9  16951  prmgaplem3  17015  prmgaplem4  17016  cshwshashlem2  17058  setsstruct2  17135  ismred  17555  isfuncd  17823  homdmcoa  18025  isdrs2  18263  fpwipodrs  18497  ipodrsima  18498  chnub  18579  chnso  18581  sgrp2rid2ex  18889  subgid  19095  issubg2  19108  subsubg  19116  gaorber  19274  orbsta  19279  pmtrfconj  19432  psgnunilem2  19461  psgnunilem3  19462  psgnunilem4  19463  pgpfi1  19561  subgpgp  19563  pgpssslw  19580  subgslw  19582  sylow2alem2  19584  fislw  19591  sylow3lem3  19595  efgs1  19701  efgsp1  19703  efgsres  19704  efgredleme  19709  efgcpbllemb  19721  lt6abl  19861  telgsumfzs  19955  ablfac1eu  20041  submomnd  20098  isrngd  20145  prdsrngd  20148  ringrng  20257  isringrng  20259  isringd  20263  ringsrg  20269  ring1  20282  prdsringd  20291  subrngid  20517  subrngsubg  20520  issubrng2  20526  subsubrng  20531  subrgsubg  20545  subrgsubrng  20546  sdrgid  20760  cntzsdrg  20770  subdrgint  20771  sdrgint  20772  suborng  20844  islmodd  20852  islssd  20921  islss4  20948  dflidl2rng  21208  rnglidl0  21219  rnglidl1  21222  rnglidlrng  21237  rng2idlsubrng  21255  rhmpreimaidl  21267  gzrngunit  21423  expmhm  21426  zringunit  21456  prmirredlem  21462  znidomb  21551  isphld  21644  ocvocv  21661  ocvlss  21662  frlmlbs  21787  psdmul  22142  gsummoncoe1  22283  mp2pm2mplem4  22784  chfacfisf  22829  chfacfisfcpmat  22830  chfacfscmulfsupp  22834  chfacfpmmulfsupp  22838  chfacfpmmulgsum2  22840  2ndcctbss  23430  finlocfin  23495  dissnlocfin  23504  locfindis  23505  locfincf  23506  isfild  23833  infil  23838  neifil  23855  flimfcls  24001  istgp2  24066  oppgtmd  24072  oppgtgp  24073  distgp  24074  indistgp  24075  efmndtmd  24076  submtmd  24079  subgtgp  24080  symgtgp  24081  qustgplem  24096  prdstmdd  24099  prdstgpd  24100  tlmtgp  24171  isngp4  24587  subgngp  24610  ngptgp  24611  tngngp2  24627  nrgtrg  24665  nrgtdrg  24668  elii2  24913  icopnfcnv  24919  xrhmeo  24923  lebnumii  24943  phtpcer  24972  reparpht  24975  phtpcco2  24976  pcohtpy  24997  pcoass  25001  pcorevlem  25003  isclmi  25054  isncvsngpd  25127  cphsubrglem  25154  cphclm  25166  phclm  25209  tcphcph  25214  clsocv  25227  cphsscph  25228  cmslssbn  25349  pjthlem2  25415  ovolf  25459  iundisj2  25526  vitalilem2  25586  vitali  25590  itg2monolem3  25729  dvfsumlem1  26003  dvfsumlem3  26005  mon1puc1p  26126  uc1pmon1p  26127  mon1pid  26129  ply1remlem  26140  drnguc1p  26149  plyaddlem1  26188  coeidlem  26212  aannenlem2  26306  radcnvcl  26395  pilem2  26430  coseq00topi  26479  coseq0negpitopi  26480  tangtx  26482  tanabsge  26483  cosq14gt0  26487  cosq14ge0  26488  cosq34lt1  26504  cosordlem  26507  cos0pilt1  26509  sinord  26511  resinf1o  26513  tanord1  26514  tanord  26515  efif1olem3  26521  efsubm  26528  relogrn  26538  logimclad  26549  logrnaddcl  26551  logneg  26565  logcj  26583  argregt0  26587  argrege0  26588  argimgt0  26589  argimlt0  26590  logimul  26591  logneg2  26592  logdmnrp  26618  logcnlem4  26622  dvloglem  26625  logf1o2  26627  efopnlem2  26634  cxpsqrtlem  26679  relogbval  26749  nnlogbexp  26758  relogbcxp  26762  relogbcxpb  26764  logbgt0b  26770  asinneg  26863  asinsin  26869  acoscos  26870  acosbnd  26877  atancj  26887  atanlogaddlem  26890  atanlogsublem  26892  atanlogsub  26893  atantan  26900  atanbndlem  26902  atans2  26908  leibpi  26919  scvxcvx  26963  jensenlem2  26965  emcllem7  26979  basellem1  27058  ppisval  27081  chtdif  27135  ppidif  27140  ppiub  27181  chtublem  27188  chtub  27189  lgsdilem2  27310  gausslemma2dlem1a  27342  gausslemma2dlem2  27344  gausslemma2dlem5  27348  gausslemma2dlem6  27349  lgsquadlem1  27357  lgsquadlem2  27358  lgsquadlem3  27359  2lgslem1  27371  2sqlem3  27397  chebbnd1lem1  27446  chebbnd1lem2  27447  chebbnd1lem3  27448  dchrisumlem2  27467  dchrvmasumlem2  27475  dchrvmasumiflem1  27478  dchrisum0flblem2  27486  mulog2sumlem2  27512  logdivbnd  27533  pntpbnd2  27564  pntibndlem1  27566  pntibnd  27570  pntlemc  27572  pntlemg  27575  pntlemq  27578  pntlemf  27582  padicabvf  27608  padicabvcxp  27609  ostth2  27614  noextend  27644  noextendseq  27645  nosupno  27681  noinfno  27696  ttgcontlem1  28967  axpaschlem  29023  nbgr2vtx1edg  29433  nbuhgr2vtx1edgb  29435  cusgrexi  29526  structtocusgr  29529  pthdadjvtx  29811  pthdlem1  29849  pthd  29852  crctcshwlkn0lem3  29895  crctcshwlkn0lem4  29896  crctcshwlkn0lem5  29897  crctcshwlkn0lem7  29899  wlkiswwlks1  29950  wwlksm1edg  29964  wwlksnred  29975  wwlksnredwwlkn  29978  wwlksnextproplem3  29994  clwlkclwwlklem2fv1  30080  clwlkclwwlklem2fv2  30081  clwlkclwwlklem2a  30083  clwlkclwwlklem2  30085  clwwisshclwwslemlem  30098  clwwisshclwwslem  30099  erclwwlkref  30105  clwwlkel  30131  clwwlkf  30132  wwlksext2clwwlk  30142  wwlksubclwwlk  30143  umgr2cwwkdifex  30150  1pthd  30228  eucrctshift  30328  dlwwlknondlwlknonf1olem1  30449  numclwlk2lem2f  30462  frgrreggt1  30478  grpoinvf  30618  strlem3a  32338  hstrlem3a  32346  iundisj2f  32675  fcoinver  32689  fresf1o  32719  ssnnssfz  32875  bcm1n  32883  iundisj2fi  32885  fsumrp0cl  33096  cycpmco2lem6  33207  fxpsdrg  33251  lmodslmd  33280  fldgensdrg  33390  intlidl  33495  idlinsubrg  33506  rhmimaidl  33507  ssdifidllem  33531  ssmxidllem  33548  1arithidomlem1  33610  1arithidomlem2  33611  1arithidom  33612  fldextsdrg  33814  fldextrspunlem2  33837  fldextrspundgdvdslem  33840  fldextrspundgdvds  33841  minplyirred  33871  algextdeglem4  33880  algextdeglem8  33884  rtelextdg2lem  33886  constrsdrg  33935  2sqr3minply  33940  cos9thpiminply  33948  locfinreflem  34000  locfinref  34001  xrge0iifcnv  34093  xrge0iifiso  34095  xrge0iifhom  34097  esumc  34211  esumle  34218  esumlef  34222  esumpinfsum  34237  esumpcvgval  34238  fiunelros  34334  voliune  34389  volfiniune  34390  sibfinima  34499  eulerpartlemt  34531  fiblem  34558  fibp1  34561  dstrvprob  34632  ballotlemsel1i  34673  ballotlemfrceq  34689  plymulx0  34707  signstfvc  34734  signstfveq0  34737  bnj944  35096  bnj998  35115  bnj1136  35155  bnj1408  35194  erdszelem4  35392  erdszelem8  35396  txsconnlem  35438  cvxsconn  35441  cvmliftpht  35516  snmlff  35527  elmrsubrn  35718  msrf  35740  mthmpps  35780  sinccvglem  35870  trer  36514  poimirlem6  37961  poimirlem7  37962  poimirlem9  37964  poimirlem17  37972  poimirlem20  37975  poimirlem28  37983  poimirlem29  37984  poimirlem30  37985  poimirlem31  37986  poimirlem32  37987  areacirc  38048  nnubfi  38085  prter1  39339  lkrlss  39555  diaf11N  41509  dibf11N  41621  lclkr  41993  lclkrs  41999  lcfrlem9  42010  lcfr  42045  mapd1o  42108  hdmapf1oN  42325  hgmapf1oN  42363  frlmvscadiccat  42965  fimgmcyc  42993  nacsfix  43158  eldioph2lem1  43206  irrapxlem1  43268  rmxypairf1o  43357  jm2.27a  43451  hbtlem2  43570  hbt  43576  mon1psubm  43645  onnoxpg  43874  pren2d  44001  binomcxplemnotnn0  44801  elixpconstg  45537  elfzfzo  45728  monoords  45748  eluzd  45855  fmul01lt1lem2  46033  sumnnodd  46078  ioodvbdlimc1lem2  46378  ioodvbdlimc2lem  46380  iblsplit  46412  iblspltprt  46419  itgspltprt  46425  stoweidlem11  46457  stoweidlem17  46463  fourierdlem12  46565  fourierdlem20  46573  fourierdlem25  46578  fourierdlem37  46590  fourierdlem41  46594  fourierdlem48  46600  fourierdlem49  46601  fourierdlem50  46602  fourierdlem54  46606  fourierdlem64  46616  fourierdlem73  46625  fourierdlem79  46631  fourierdlem102  46654  fourierdlem111  46663  fourierdlem114  46666  etransclem23  46703  etransclem48  46728  ormkglobd  47321  chnsubseq  47326  2elfz2melfz  47778  elfzlble  47780  ceilhalfelfzo1  47794  1elfzo1ceilhalf1  47801  difltmodne  47808  modm2nep1  47832  modm1nep2  47834  modm1p1ne  47836  iccpartiltu  47894  iccpartigtl  47895  iccpartlt  47896  iccpartgt  47899  lswn0  47916  fmtnoge3  48005  fmtnodvds  48019  odz2prm2pw  48038  fmtnole4prm  48053  lighneallem4b  48084  nprmdvdsfacm1lem3  48097  nprmdvdsfacm1lem4  48098  nprmdvdsfacm1  48099  mogoldbb  48273  nnsum4primesevenALTV  48289  bgoldbtbndlem3  48295  gpgprismgriedgdmss  48540  gpgprismgrusgra  48546  gpg3nbgrvtx0  48564  gpg3nbgrvtx0ALT  48565  gpg5nbgrvtx03star  48568  gpg5nbgr3star  48569  gpg3kgrtriexlem3  48573  gpg3kgrtriexlem4  48574  gpg3kgrtriexlem6  48576  gpgprismgr4cycllem3  48585  gpgprismgr4cycllem9  48591  ssnn0ssfz  48837  lmod1  48980  elfzolborelfzop1  49007  nnolog2flm1  49078  funcf2lem2  49569  isnatd  49710