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  7273  limuni3  7794  onfununi  8272  smores2  8285  smoiso  8293  oelimcl  8527  iserd  8661  resixp  8872  undifixp  8873  alephval3  10021  canthwelem  10562  canthwe  10563  r1limwun  10648  wunex2  10650  tskcard  10693  gruina  10730  eluzmn  12784  eluzuzle  12786  uztrn  12795  eluzadd  12806  eluzsub  12807  subeluzsub  12810  nn0pzuz  12844  zsupss  12876  nn0ge2m1nnALT  12881  xov1plusxeqvd  13440  ige2m1fz  13560  0elfz  13567  uzsubfz0  13579  elfzmlbm  13581  difelfzle  13584  difelfznle  13585  fvffz0  13589  elfzod  13606  elfzolt2b  13614  elfzolt3b  13615  elfzouz2  13618  fzossrbm1  13632  elfzo0  13644  eluzgtdifelfzo  13671  elfzodifsumelfzo  13675  fzonn0p1  13686  fzonn0p1p1  13688  fzo0sn0fzo1  13699  ssfzo12bi  13705  fzoopth  13706  ubmelm1fzo  13707  elfzonelfzo  13713  fzosplitprm1  13722  fzostep1  13730  fvinim0ffz  13733  flword2  13761  uzsup  13811  modfzo0difsn  13894  modsumfzodifsn  13895  fsuppmapnn0fiub  13942  suppssfz  13945  1elfz0hash  14341  fzsdom2  14379  ccatdmss  14533  ccatrn  14541  ccat2s1fvw  14590  pfxn0  14638  pfxtrcfv0  14645  pfxtrcfvl  14648  swrdswrd  14656  swrdccatin1  14676  pfxccat3  14685  pfxccat3a  14689  repswswrd  14735  cshwidxmod  14754  cshw1  14773  cshwcsh2id  14779  swrds2  14891  pfx2  14898  2swrd2eqwrdeq  14904  ccat2s1fvwALT  14906  rexuzre  15304  limsupgre  15432  rlimclim1  15496  rlimclim  15497  climrlim2  15498  isercolllem1  15616  isercoll  15619  climcndslem1  15803  fallfacval4  15997  tanhbnd  16117  sinbnd2  16138  cosbnd2  16139  rpnnen2lem12  16181  nn0o  16341  bitsfzolem  16392  bitsfzo  16393  bitsmod  16394  bitsfi  16395  bitsinv1lem  16399  bitsinv1  16400  smueqlem  16448  dvdsnprmd  16648  2mulprm  16651  hashgcdlem  16747  prm23lt5  16774  zgz  16893  gznegcl  16895  gzcjcl  16896  gzaddcl  16897  gzmulcl  16898  vdwlem9  16949  prmgaplem3  17013  prmgaplem4  17014  cshwshashlem2  17056  setsstruct2  17133  ismred  17553  isfuncd  17821  homdmcoa  18023  isdrs2  18261  fpwipodrs  18495  ipodrsima  18496  chnub  18577  chnso  18579  sgrp2rid2ex  18887  subgid  19093  issubg2  19106  subsubg  19114  gaorber  19272  orbsta  19277  pmtrfconj  19430  psgnunilem2  19459  psgnunilem3  19460  psgnunilem4  19461  pgpfi1  19559  subgpgp  19561  pgpssslw  19578  subgslw  19580  sylow2alem2  19582  fislw  19589  sylow3lem3  19593  efgs1  19699  efgsp1  19701  efgsres  19702  efgredleme  19707  efgcpbllemb  19719  lt6abl  19859  telgsumfzs  19953  ablfac1eu  20039  submomnd  20096  isrngd  20143  prdsrngd  20146  ringrng  20255  isringrng  20257  isringd  20261  ringsrg  20267  ring1  20280  prdsringd  20289  subrngid  20515  subrngsubg  20518  issubrng2  20524  subsubrng  20529  subrgsubg  20543  subrgsubrng  20544  sdrgid  20758  cntzsdrg  20768  subdrgint  20769  sdrgint  20770  suborng  20842  islmodd  20850  islssd  20919  islss4  20946  dflidl2rng  21206  rnglidl0  21217  rnglidl1  21220  rnglidlrng  21235  rng2idlsubrng  21253  rhmpreimaidl  21265  gzrngunit  21421  expmhm  21424  zringunit  21454  prmirredlem  21460  znidomb  21549  isphld  21642  ocvocv  21659  ocvlss  21660  frlmlbs  21785  psdmul  22141  gsummoncoe1  22282  mp2pm2mplem4  22783  chfacfisf  22828  chfacfisfcpmat  22829  chfacfscmulfsupp  22833  chfacfpmmulfsupp  22837  chfacfpmmulgsum2  22839  2ndcctbss  23429  finlocfin  23494  dissnlocfin  23503  locfindis  23504  locfincf  23505  isfild  23832  infil  23837  neifil  23854  flimfcls  24000  istgp2  24065  oppgtmd  24071  oppgtgp  24072  distgp  24073  indistgp  24074  efmndtmd  24075  submtmd  24078  subgtgp  24079  symgtgp  24080  qustgplem  24095  prdstmdd  24098  prdstgpd  24099  tlmtgp  24170  isngp4  24586  subgngp  24609  ngptgp  24610  tngngp2  24626  nrgtrg  24664  nrgtdrg  24667  elii2  24912  icopnfcnv  24918  xrhmeo  24922  lebnumii  24942  phtpcer  24971  reparpht  24974  phtpcco2  24975  pcohtpy  24996  pcoass  25000  pcorevlem  25002  isclmi  25053  isncvsngpd  25126  cphsubrglem  25153  cphclm  25165  phclm  25208  tcphcph  25213  clsocv  25226  cphsscph  25227  cmslssbn  25348  pjthlem2  25414  ovolf  25458  iundisj2  25525  vitalilem2  25585  vitali  25589  itg2monolem3  25728  dvfsumlem1  26004  dvfsumlem3  26007  mon1puc1p  26128  uc1pmon1p  26129  mon1pid  26131  ply1remlem  26142  drnguc1p  26151  plyaddlem1  26190  coeidlem  26214  aannenlem2  26308  radcnvcl  26397  pilem2  26433  coseq00topi  26482  coseq0negpitopi  26483  tangtx  26485  tanabsge  26486  cosq14gt0  26490  cosq14ge0  26491  cosq34lt1  26507  cosordlem  26510  cos0pilt1  26512  sinord  26514  resinf1o  26516  tanord1  26517  tanord  26518  efif1olem3  26524  efsubm  26531  relogrn  26541  logimclad  26552  logrnaddcl  26554  logneg  26568  logcj  26586  argregt0  26590  argrege0  26591  argimgt0  26592  argimlt0  26593  logimul  26594  logneg2  26595  logdmnrp  26621  logcnlem4  26625  dvloglem  26628  logf1o2  26630  efopnlem2  26637  cxpsqrtlem  26682  relogbval  26753  nnlogbexp  26762  relogbcxp  26766  relogbcxpb  26768  logbgt0b  26774  asinneg  26867  asinsin  26873  acoscos  26874  acosbnd  26881  atancj  26891  atanlogaddlem  26894  atanlogsublem  26896  atanlogsub  26897  atantan  26904  atanbndlem  26906  atans2  26912  leibpi  26923  scvxcvx  26967  jensenlem2  26969  emcllem7  26983  basellem1  27062  ppisval  27085  chtdif  27139  ppidif  27144  ppiub  27186  chtublem  27193  chtub  27194  lgsdilem2  27315  gausslemma2dlem1a  27347  gausslemma2dlem2  27349  gausslemma2dlem5  27353  gausslemma2dlem6  27354  lgsquadlem1  27362  lgsquadlem2  27363  lgsquadlem3  27364  2lgslem1  27376  2sqlem3  27402  chebbnd1lem1  27451  chebbnd1lem2  27452  chebbnd1lem3  27453  dchrisumlem2  27472  dchrvmasumlem2  27480  dchrvmasumiflem1  27483  dchrisum0flblem2  27491  mulog2sumlem2  27517  logdivbnd  27538  pntpbnd2  27569  pntibndlem1  27571  pntibnd  27575  pntlemc  27577  pntlemg  27580  pntlemq  27583  pntlemf  27587  padicabvf  27613  padicabvcxp  27614  ostth2  27619  noextend  27649  noextendseq  27650  nosupno  27686  noinfno  27701  ttgcontlem1  28972  axpaschlem  29028  nbgr2vtx1edg  29438  nbuhgr2vtx1edgb  29440  cusgrexi  29531  structtocusgr  29534  pthdadjvtx  29816  pthdlem1  29854  pthd  29857  crctcshwlkn0lem3  29900  crctcshwlkn0lem4  29901  crctcshwlkn0lem5  29902  crctcshwlkn0lem7  29904  wlkiswwlks1  29955  wwlksm1edg  29969  wwlksnred  29980  wwlksnredwwlkn  29983  wwlksnextproplem3  29999  clwlkclwwlklem2fv1  30085  clwlkclwwlklem2fv2  30086  clwlkclwwlklem2a  30088  clwlkclwwlklem2  30090  clwwisshclwwslemlem  30103  clwwisshclwwslem  30104  erclwwlkref  30110  clwwlkel  30136  clwwlkf  30137  wwlksext2clwwlk  30147  wwlksubclwwlk  30148  umgr2cwwkdifex  30155  1pthd  30233  eucrctshift  30333  dlwwlknondlwlknonf1olem1  30454  numclwlk2lem2f  30467  frgrreggt1  30483  grpoinvf  30623  strlem3a  32343  hstrlem3a  32351  iundisj2f  32680  fcoinver  32694  fresf1o  32724  ssnnssfz  32880  bcm1n  32888  iundisj2fi  32890  fsumrp0cl  33101  cycpmco2lem6  33212  fxpsdrg  33256  lmodslmd  33285  fldgensdrg  33395  intlidl  33500  idlinsubrg  33511  rhmimaidl  33512  ssdifidllem  33536  ssmxidllem  33553  1arithidomlem1  33615  1arithidomlem2  33616  1arithidom  33617  fldextsdrg  33819  fldextrspunlem2  33842  fldextrspundgdvdslem  33845  fldextrspundgdvds  33846  minplyirred  33876  algextdeglem4  33885  algextdeglem8  33889  rtelextdg2lem  33891  constrsdrg  33940  2sqr3minply  33945  cos9thpiminply  33953  locfinreflem  34005  locfinref  34006  xrge0iifcnv  34098  xrge0iifiso  34100  xrge0iifhom  34102  esumc  34216  esumle  34223  esumlef  34227  esumpinfsum  34242  esumpcvgval  34243  fiunelros  34339  voliune  34394  volfiniune  34395  sibfinima  34504  eulerpartlemt  34536  fiblem  34563  fibp1  34566  dstrvprob  34637  ballotlemsel1i  34678  ballotlemfrceq  34694  plymulx0  34712  signstfvc  34739  signstfveq0  34742  bnj944  35101  bnj998  35120  bnj1136  35160  bnj1408  35199  erdszelem4  35397  erdszelem8  35401  txsconnlem  35443  cvxsconn  35446  cvmliftpht  35521  snmlff  35532  elmrsubrn  35723  msrf  35745  mthmpps  35785  sinccvglem  35875  trer  36519  poimirlem6  37958  poimirlem7  37959  poimirlem9  37961  poimirlem17  37969  poimirlem20  37972  poimirlem28  37980  poimirlem29  37981  poimirlem30  37982  poimirlem31  37983  poimirlem32  37984  areacirc  38045  nnubfi  38082  prter1  39336  lkrlss  39552  diaf11N  41506  dibf11N  41618  lclkr  41990  lclkrs  41996  lcfrlem9  42007  lcfr  42042  mapd1o  42105  hdmapf1oN  42322  hgmapf1oN  42360  frlmvscadiccat  42962  fimgmcyc  42990  nacsfix  43155  eldioph2lem1  43203  irrapxlem1  43265  rmxypairf1o  43354  jm2.27a  43448  hbtlem2  43567  hbt  43573  mon1psubm  43642  onnoxpg  43871  pren2d  43998  binomcxplemnotnn0  44798  elixpconstg  45534  elfzfzo  45725  monoords  45745  eluzd  45852  fmul01lt1lem2  46030  sumnnodd  46075  ioodvbdlimc1lem2  46375  ioodvbdlimc2lem  46377  iblsplit  46409  iblspltprt  46416  itgspltprt  46422  stoweidlem11  46454  stoweidlem17  46460  fourierdlem12  46562  fourierdlem20  46570  fourierdlem25  46575  fourierdlem37  46587  fourierdlem41  46591  fourierdlem48  46597  fourierdlem49  46598  fourierdlem50  46599  fourierdlem54  46603  fourierdlem64  46613  fourierdlem73  46622  fourierdlem79  46628  fourierdlem102  46651  fourierdlem111  46660  fourierdlem114  46663  etransclem23  46700  etransclem48  46725  ormkglobd  47318  chnsubseq  47323  2elfz2melfz  47763  elfzlble  47765  ceilhalfelfzo1  47779  1elfzo1ceilhalf1  47786  difltmodne  47793  modm2nep1  47817  modm1nep2  47819  modm1p1ne  47821  iccpartiltu  47879  iccpartigtl  47880  iccpartlt  47881  iccpartgt  47884  lswn0  47901  fmtnoge3  47990  fmtnodvds  48004  odz2prm2pw  48023  fmtnole4prm  48038  lighneallem4b  48069  nprmdvdsfacm1lem3  48082  nprmdvdsfacm1lem4  48083  nprmdvdsfacm1  48084  mogoldbb  48258  nnsum4primesevenALTV  48274  bgoldbtbndlem3  48280  gpgprismgriedgdmss  48525  gpgprismgrusgra  48531  gpg3nbgrvtx0  48549  gpg3nbgrvtx0ALT  48550  gpg5nbgrvtx03star  48553  gpg5nbgr3star  48554  gpg3kgrtriexlem3  48558  gpg3kgrtriexlem4  48559  gpg3kgrtriexlem6  48561  gpgprismgr4cycllem3  48570  gpgprismgr4cycllem9  48576  ssnn0ssfz  48822  lmod1  48965  elfzolborelfzop1  48992  nnolog2flm1  49063  funcf2lem2  49554  isnatd  49695