Theorem syl3anbrc 1339

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  soisores  7080  limuni3  7567  onfununi  7978  smores2  7991  smoiso  7999  oelimcl  8226  iserd  8315  resixp  8497  undifixp  8498  alephval3  9536  canthwelem  10072  canthwe  10073  r1limwun  10158  wunex2  10160  tskcard  10203  gruina  10240  eluzmn  12251  eluzuzle  12253  uztrn  12262  subeluzsub  12276  nn0pzuz  12306  zsupss  12338  nn0ge2m1nnALT  12343  xov1plusxeqvd  12885  ssfzunsnext  12953  ige2m1fz  12998  0elfz  13005  uzsubfz0  13016  elfzmlbm  13018  difelfzle  13021  difelfznle  13022  fvffz0  13026  elfzolt2b  13050  elfzolt3b  13051  elfzouz2  13053  fzossrbm1  13067  elfzo0  13079  eluzgtdifelfzo  13100  elfzodifsumelfzo  13104  fzonn0p1  13115  fzonn0p1p1  13117  fzo0sn0fzo1  13127  ssfzo12bi  13133  ubmelm1fzo  13134  elfzonelfzo  13140  fzosplitprm1  13148  fzostep1  13154  fvinim0ffz  13157  flword2  13184  uzsup  13232  modfzo0difsn  13312  modsumfzodifsn  13313  fsuppmapnn0fiub  13360  suppssfz  13363  1elfz0hash  13752  fzsdom2  13790  ccatrn  13943  ccat2s1fvw  13998  ccat2s1fvwOLD  13999  pfxn0  14048  pfxtrcfv0  14056  pfxtrcfvl  14059  swrdswrd  14067  swrdccatin1  14087  pfxccat3  14096  pfxccat3a  14100  repswswrd  14146  cshwidxmod  14165  cshw1  14184  cshwcsh2id  14190  swrds2  14302  pfx2  14309  2swrd2eqwrdeq  14315  ccat2s1fvwALT  14318  ccat2s1fvwALTOLD  14319  rexuzre  14712  limsupgre  14838  rlimclim1  14902  rlimclim  14903  climrlim2  14904  isercolllem1  15021  isercoll  15024  climcndslem1  15204  fallfacval4  15397  tanhbnd  15514  sinbnd2  15535  cosbnd2  15536  rpnnen2lem12  15578  nn0o  15734  bitsfzolem  15783  bitsfzo  15784  bitsmod  15785  bitsfi  15786  bitsinv1lem  15790  bitsinv1  15791  smueqlem  15839  dvdsnprmd  16034  2mulprm  16037  hashgcdlem  16125  prm23lt5  16151  zgz  16269  gznegcl  16271  gzcjcl  16272  gzaddcl  16273  gzmulcl  16274  vdwlem9  16325  prmgaplem3  16389  prmgaplem4  16390  cshwshashlem2  16430  setsstruct2  16521  ismred  16873  isfuncd  17135  homdmcoa  17327  isdrs2  17549  fpwipodrs  17774  ipodrsima  17775  sgrp2rid2ex  18092  subgid  18281  issubg2  18294  subsubg  18302  gaorber  18438  orbsta  18443  pmtrfconj  18594  psgnunilem2  18623  psgnunilem3  18624  psgnunilem4  18625  pgpfi1  18720  subgpgp  18722  pgpssslw  18739  subgslw  18741  sylow2alem2  18743  fislw  18750  sylow3lem3  18754  efgs1  18861  efgsp1  18863  efgsres  18864  efgredleme  18869  efgcpbllemb  18881  lt6abl  19015  telgsumfzs  19109  ablfac1eu  19195  isringd  19335  ringsrg  19339  ring1  19352  prdsringd  19362  subrgsubg  19541  sdrgid  19575  cntzsdrg  19581  subdrgint  19582  sdrgint  19583  islmodd  19640  islssd  19707  islss4  19734  gsummoncoe1  20472  gzrngunit  20611  expmhm  20614  zringunit  20635  prmirredlem  20640  znidomb  20708  isphld  20798  ocvocv  20815  ocvlss  20816  frlmlbs  20941  mp2pm2mplem4  21417  chfacfisf  21462  chfacfisfcpmat  21463  chfacfscmulfsupp  21467  chfacfpmmulfsupp  21471  chfacfpmmulgsum2  21473  2ndcctbss  22063  finlocfin  22128  dissnlocfin  22137  locfindis  22138  locfincf  22139  isfild  22466  infil  22471  neifil  22488  flimfcls  22634  istgp2  22699  oppgtmd  22705  oppgtgp  22706  distgp  22707  indistgp  22708  efmndtmd  22709  submtmd  22712  subgtgp  22713  symgtgp  22714  qustgplem  22729  prdstmdd  22732  prdstgpd  22733  tlmtgp  22804  isngp4  23221  subgngp  23244  ngptgp  23245  tngngp2  23261  nrgtrg  23299  nrgtdrg  23302  elii2  23540  icopnfcnv  23546  xrhmeo  23550  lebnumii  23570  phtpcer  23599  reparpht  23602  phtpcco2  23603  pcohtpy  23624  pcoass  23628  pcorevlem  23630  isclmi  23681  isncvsngpd  23754  cphsubrglem  23781  cphclm  23793  phclm  23835  tcphcph  23840  clsocv  23853  cphsscph  23854  cmslssbn  23975  pjthlem2  24041  ovolf  24083  iundisj2  24150  vitalilem2  24210  vitali  24214  itg2monolem3  24353  dvfsumlem1  24623  dvfsumlem3  24625  mon1puc1p  24744  uc1pmon1p  24745  ply1remlem  24756  drnguc1p  24764  plyaddlem1  24803  coeidlem  24827  aannenlem2  24918  radcnvcl  25005  pilem2  25040  coseq00topi  25088  coseq0negpitopi  25089  tangtx  25091  tanabsge  25092  cosq14gt0  25096  cosq14ge0  25097  cosq34lt1  25112  cosordlem  25115  sinord  25118  resinf1o  25120  tanord1  25121  tanord  25122  efif1olem3  25128  efsubm  25135  relogrn  25145  logimclad  25156  logrnaddcl  25158  logneg  25171  logcj  25189  argregt0  25193  argrege0  25194  argimgt0  25195  argimlt0  25196  logimul  25197  logneg2  25198  logdmnrp  25224  logcnlem4  25228  dvloglem  25231  logf1o2  25233  efopnlem2  25240  cxpsqrtlem  25285  relogbval  25350  nnlogbexp  25359  relogbcxp  25363  relogbcxpb  25365  logbgt0b  25371  asinneg  25464  asinsin  25470  acoscos  25471  acosbnd  25478  atancj  25488  atanlogaddlem  25491  atanlogsublem  25493  atanlogsub  25494  atantan  25501  atanbndlem  25503  atans2  25509  leibpi  25520  scvxcvx  25563  jensenlem2  25565  emcllem7  25579  basellem1  25658  ppisval  25681  chtdif  25735  ppidif  25740  ppiub  25780  chtublem  25787  chtub  25788  lgsdilem2  25909  gausslemma2dlem1a  25941  gausslemma2dlem2  25943  gausslemma2dlem5  25947  gausslemma2dlem6  25948  lgsquadlem1  25956  lgsquadlem2  25957  lgsquadlem3  25958  2lgslem1  25970  2sqlem3  25996  chebbnd1lem1  26045  chebbnd1lem2  26046  chebbnd1lem3  26047  dchrisumlem2  26066  dchrvmasumlem2  26074  dchrvmasumiflem1  26077  dchrisum0flblem2  26085  mulog2sumlem2  26111  logdivbnd  26132  pntpbnd2  26163  pntibndlem1  26165  pntibnd  26169  pntlemc  26171  pntlemg  26174  pntlemq  26177  pntlemf  26181  padicabvf  26207  padicabvcxp  26208  ostth2  26213  ttgcontlem1  26671  axpaschlem  26726  nbgr2vtx1edg  27132  nbuhgr2vtx1edgb  27134  cusgrexi  27225  structtocusgr  27228  pthdadjvtx  27511  pthdlem1  27547  pthd  27550  crctcshwlkn0lem3  27590  crctcshwlkn0lem4  27591  crctcshwlkn0lem5  27592  crctcshwlkn0lem7  27594  wlkiswwlks1  27645  wwlksm1edg  27659  wwlksnred  27670  wwlksnredwwlkn  27673  wwlksnextproplem3  27690  clwlkclwwlklem2fv1  27773  clwlkclwwlklem2fv2  27774  clwlkclwwlklem2a  27776  clwlkclwwlklem2  27778  clwwisshclwwslemlem  27791  clwwisshclwwslem  27792  erclwwlkref  27798  clwwlkel  27825  clwwlkf  27826  wwlksext2clwwlk  27836  wwlksubclwwlk  27837  umgr2cwwkdifex  27844  1pthd  27922  eucrctshift  28022  dlwwlknondlwlknonf1olem1  28143  numclwlk2lem2f  28156  frgrreggt1  28172  grpoinvf  28309  strlem3a  30029  hstrlem3a  30037  iundisj2f  30340  fcoinver  30357  fresf1o  30376  ssnnssfz  30510  bcm1n  30518  iundisj2fi  30520  fsumrp0cl  30682  submomnd  30711  cycpmco2lem6  30773  lmodslmd  30832  suborng  30888  ssmxidllem  30978  locfinreflem  31104  locfinref  31105  xrge0iifcnv  31176  xrge0iifiso  31178  xrge0iifhom  31180  esumc  31310  esumle  31317  esumlef  31321  esumpinfsum  31336  esumpcvgval  31337  fiunelros  31433  voliune  31488  volfiniune  31489  sibfinima  31597  eulerpartlemt  31629  fiblem  31656  fibp1  31659  dstrvprob  31729  ballotlemsel1i  31770  ballotlemfrceq  31786  plymulx0  31817  signstfvc  31844  signstfveq0  31847  bnj944  32210  bnj998  32229  bnj1136  32269  bnj1408  32308  erdszelem4  32441  erdszelem8  32445  txsconnlem  32487  cvxsconn  32490  cvmliftpht  32565  snmlff  32576  elmrsubrn  32767  msrf  32789  mthmpps  32829  sinccvglem  32915  noextend  33173  noextendseq  33174  nosupno  33203  trer  33664  poimirlem6  34913  poimirlem7  34914  poimirlem9  34916  poimirlem17  34924  poimirlem20  34927  poimirlem28  34935  poimirlem29  34936  poimirlem30  34937  poimirlem31  34938  poimirlem32  34939  areacirc  35002  nnubfi  35040  prter1  36030  lkrlss  36246  diaf11N  38200  dibf11N  38312  lclkr  38684  lclkrs  38690  lcfrlem9  38701  lcfr  38736  mapd1o  38799  hdmapf1oN  39016  hgmapf1oN  39054  frlmvscadiccat  39194  nacsfix  39358  eldioph2lem1  39406  irrapxlem1  39468  rmxypairf1o  39557  jm2.27a  39651  hbtlem2  39773  hbt  39779  mon1pid  39854  mon1psubm  39855  pren2d  39964  binomcxplemnotnn0  40737  elixpconstg  41404  elfzfzo  41591  monoords  41613  elfzod  41722  eluzd  41731  fmul01lt1lem2  41915  sumnnodd  41960  ioodvbdlimc1lem2  42266  ioodvbdlimc2lem  42268  iblsplit  42300  iblspltprt  42307  itgspltprt  42313  stoweidlem11  42345  stoweidlem17  42351  fourierdlem12  42453  fourierdlem20  42461  fourierdlem25  42466  fourierdlem37  42478  fourierdlem41  42482  fourierdlem48  42488  fourierdlem49  42489  fourierdlem50  42490  fourierdlem54  42494  fourierdlem64  42504  fourierdlem73  42513  fourierdlem79  42519  fourierdlem102  42542  fourierdlem111  42551  fourierdlem114  42554  etransclem23  42591  etransclem48  42616  2elfz2melfz  43567  elfzlble  43569  fzoopth  43576  iccpartiltu  43631  iccpartigtl  43632  iccpartlt  43633  iccpartgt  43636  lswn0  43653  fmtnoge3  43741  fmtnodvds  43755  odz2prm2pw  43774  fmtnole4prm  43789  lighneallem4b  43823  mogoldbb  43999  nnsum4primesevenALTV  44015  bgoldbtbndlem3  44021  ringrng  44199  isringrng  44201  lidlrng  44247  ssnn0ssfz  44446  lmod1  44596  elfzolborelfzop1  44623  nnolog2flm1  44699