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  7268  limuni3  7792  onfununi  8271  smores2  8284  smoiso  8292  oelimcl  8525  iserd  8658  resixp  8867  undifixp  8868  alephval3  10023  canthwelem  10563  canthwe  10564  r1limwun  10649  wunex2  10651  tskcard  10694  gruina  10731  eluzmn  12760  eluzuzle  12762  uztrn  12771  eluzadd  12782  eluzsub  12783  subeluzsub  12790  nn0pzuz  12824  zsupss  12856  nn0ge2m1nnALT  12861  xov1plusxeqvd  13419  ige2m1fz  13538  0elfz  13545  uzsubfz0  13557  elfzmlbm  13559  difelfzle  13562  difelfznle  13563  fvffz0  13567  elfzolt2b  13591  elfzolt3b  13592  elfzouz2  13595  fzossrbm1  13609  elfzo0  13621  eluzgtdifelfzo  13648  elfzodifsumelfzo  13652  fzonn0p1  13663  fzonn0p1p1  13665  fzo0sn0fzo1  13676  ssfzo12bi  13682  fzoopth  13683  ubmelm1fzo  13684  elfzonelfzo  13690  fzosplitprm1  13698  fzostep1  13704  fvinim0ffz  13707  flword2  13735  uzsup  13785  modfzo0difsn  13868  modsumfzodifsn  13869  fsuppmapnn0fiub  13916  suppssfz  13919  1elfz0hash  14315  fzsdom2  14353  ccatrn  14514  ccat2s1fvw  14563  pfxn0  14611  pfxtrcfv0  14618  pfxtrcfvl  14621  swrdswrd  14629  swrdccatin1  14649  pfxccat3  14658  pfxccat3a  14662  repswswrd  14708  cshwidxmod  14727  cshw1  14746  cshwcsh2id  14753  swrds2  14865  pfx2  14872  2swrd2eqwrdeq  14878  ccat2s1fvwALT  14880  rexuzre  15278  limsupgre  15406  rlimclim1  15470  rlimclim  15471  climrlim2  15472  isercolllem1  15590  isercoll  15593  climcndslem1  15774  fallfacval4  15968  tanhbnd  16088  sinbnd2  16109  cosbnd2  16110  rpnnen2lem12  16152  nn0o  16312  bitsfzolem  16363  bitsfzo  16364  bitsmod  16365  bitsfi  16366  bitsinv1lem  16370  bitsinv1  16371  smueqlem  16419  dvdsnprmd  16619  2mulprm  16622  hashgcdlem  16717  prm23lt5  16744  zgz  16863  gznegcl  16865  gzcjcl  16866  gzaddcl  16867  gzmulcl  16868  vdwlem9  16919  prmgaplem3  16983  prmgaplem4  16984  cshwshashlem2  17026  setsstruct2  17103  ismred  17522  isfuncd  17790  homdmcoa  17992  isdrs2  18230  fpwipodrs  18464  ipodrsima  18465  sgrp2rid2ex  18819  subgid  19025  issubg2  19038  subsubg  19046  gaorber  19205  orbsta  19210  pmtrfconj  19363  psgnunilem2  19392  psgnunilem3  19393  psgnunilem4  19394  pgpfi1  19492  subgpgp  19494  pgpssslw  19511  subgslw  19513  sylow2alem2  19515  fislw  19522  sylow3lem3  19526  efgs1  19632  efgsp1  19634  efgsres  19635  efgredleme  19640  efgcpbllemb  19652  lt6abl  19792  telgsumfzs  19886  ablfac1eu  19972  submomnd  20029  isrngd  20076  prdsrngd  20079  ringrng  20188  isringrng  20190  isringd  20194  ringsrg  20200  ring1  20213  prdsringd  20224  subrngid  20452  subrngsubg  20455  issubrng2  20461  subsubrng  20466  subrgsubg  20480  subrgsubrng  20481  sdrgid  20695  cntzsdrg  20705  subdrgint  20706  sdrgint  20707  suborng  20779  islmodd  20787  islssd  20856  islss4  20883  dflidl2rng  21143  rnglidl0  21154  rnglidl1  21157  rnglidlrng  21172  rng2idlsubrng  21190  rhmpreimaidl  21202  gzrngunit  21358  expmhm  21361  zringunit  21391  prmirredlem  21397  znidomb  21486  isphld  21579  ocvocv  21596  ocvlss  21597  frlmlbs  21722  psdmul  22069  gsummoncoe1  22211  mp2pm2mplem4  22712  chfacfisf  22757  chfacfisfcpmat  22758  chfacfscmulfsupp  22762  chfacfpmmulfsupp  22766  chfacfpmmulgsum2  22768  2ndcctbss  23358  finlocfin  23423  dissnlocfin  23432  locfindis  23433  locfincf  23434  isfild  23761  infil  23766  neifil  23783  flimfcls  23929  istgp2  23994  oppgtmd  24000  oppgtgp  24001  distgp  24002  indistgp  24003  efmndtmd  24004  submtmd  24007  subgtgp  24008  symgtgp  24009  qustgplem  24024  prdstmdd  24027  prdstgpd  24028  tlmtgp  24099  isngp4  24516  subgngp  24539  ngptgp  24540  tngngp2  24556  nrgtrg  24594  nrgtdrg  24597  elii2  24848  icopnfcnv  24856  xrhmeo  24860  lebnumii  24881  phtpcer  24910  reparpht  24914  phtpcco2  24915  pcohtpy  24936  pcoass  24940  pcorevlem  24942  isclmi  24993  isncvsngpd  25066  cphsubrglem  25093  cphclm  25105  phclm  25148  tcphcph  25153  clsocv  25166  cphsscph  25167  cmslssbn  25288  pjthlem2  25354  ovolf  25399  iundisj2  25466  vitalilem2  25526  vitali  25530  itg2monolem3  25669  dvfsumlem1  25948  dvfsumlem3  25951  mon1puc1p  26072  uc1pmon1p  26073  mon1pid  26075  ply1remlem  26086  drnguc1p  26095  plyaddlem1  26134  coeidlem  26158  aannenlem2  26253  radcnvcl  26342  pilem2  26378  coseq00topi  26427  coseq0negpitopi  26428  tangtx  26430  tanabsge  26431  cosq14gt0  26435  cosq14ge0  26436  cosq34lt1  26452  cosordlem  26455  cos0pilt1  26457  sinord  26459  resinf1o  26461  tanord1  26462  tanord  26463  efif1olem3  26469  efsubm  26476  relogrn  26486  logimclad  26497  logrnaddcl  26499  logneg  26513  logcj  26531  argregt0  26535  argrege0  26536  argimgt0  26537  argimlt0  26538  logimul  26539  logneg2  26540  logdmnrp  26566  logcnlem4  26570  dvloglem  26573  logf1o2  26575  efopnlem2  26582  cxpsqrtlem  26627  relogbval  26698  nnlogbexp  26707  relogbcxp  26711  relogbcxpb  26713  logbgt0b  26719  asinneg  26812  asinsin  26818  acoscos  26819  acosbnd  26826  atancj  26836  atanlogaddlem  26839  atanlogsublem  26841  atanlogsub  26842  atantan  26849  atanbndlem  26851  atans2  26857  leibpi  26868  scvxcvx  26912  jensenlem2  26914  emcllem7  26928  basellem1  27007  ppisval  27030  chtdif  27084  ppidif  27089  ppiub  27131  chtublem  27138  chtub  27139  lgsdilem2  27260  gausslemma2dlem1a  27292  gausslemma2dlem2  27294  gausslemma2dlem5  27298  gausslemma2dlem6  27299  lgsquadlem1  27307  lgsquadlem2  27308  lgsquadlem3  27309  2lgslem1  27321  2sqlem3  27347  chebbnd1lem1  27396  chebbnd1lem2  27397  chebbnd1lem3  27398  dchrisumlem2  27417  dchrvmasumlem2  27425  dchrvmasumiflem1  27428  dchrisum0flblem2  27436  mulog2sumlem2  27462  logdivbnd  27483  pntpbnd2  27514  pntibndlem1  27516  pntibnd  27520  pntlemc  27522  pntlemg  27525  pntlemq  27528  pntlemf  27532  padicabvf  27558  padicabvcxp  27559  ostth2  27564  noextend  27594  noextendseq  27595  nosupno  27631  noinfno  27646  ttgcontlem1  28848  axpaschlem  28903  nbgr2vtx1edg  29313  nbuhgr2vtx1edgb  29315  cusgrexi  29406  structtocusgr  29409  pthdadjvtx  29691  pthdlem1  29729  pthd  29732  crctcshwlkn0lem3  29775  crctcshwlkn0lem4  29776  crctcshwlkn0lem5  29777  crctcshwlkn0lem7  29779  wlkiswwlks1  29830  wwlksm1edg  29844  wwlksnred  29855  wwlksnredwwlkn  29858  wwlksnextproplem3  29874  clwlkclwwlklem2fv1  29957  clwlkclwwlklem2fv2  29958  clwlkclwwlklem2a  29960  clwlkclwwlklem2  29962  clwwisshclwwslemlem  29975  clwwisshclwwslem  29976  erclwwlkref  29982  clwwlkel  30008  clwwlkf  30009  wwlksext2clwwlk  30019  wwlksubclwwlk  30020  umgr2cwwkdifex  30027  1pthd  30105  eucrctshift  30205  dlwwlknondlwlknonf1olem1  30326  numclwlk2lem2f  30339  frgrreggt1  30355  grpoinvf  30494  strlem3a  32214  hstrlem3a  32222  iundisj2f  32552  fcoinver  32566  fresf1o  32588  ssnnssfz  32743  bcm1n  32751  iundisj2fi  32753  ccatdmss  32904  chnub  32967  chnso  32969  fsumrp0cl  32988  cycpmco2lem6  33086  lmodslmd  33156  fldgensdrg  33263  intlidl  33367  idlinsubrg  33378  rhmimaidl  33379  ssdifidllem  33403  ssmxidllem  33420  1arithidomlem1  33482  1arithidomlem2  33483  1arithidom  33484  fldextsdrg  33626  fldextrspunlem2  33648  fldextrspundgdvdslem  33651  fldextrspundgdvds  33652  minplyirred  33677  algextdeglem4  33686  algextdeglem8  33690  rtelextdg2lem  33692  constrsdrg  33741  2sqr3minply  33746  cos9thpiminply  33754  locfinreflem  33806  locfinref  33807  xrge0iifcnv  33899  xrge0iifiso  33901  xrge0iifhom  33903  esumc  34017  esumle  34024  esumlef  34028  esumpinfsum  34043  esumpcvgval  34044  fiunelros  34140  voliune  34195  volfiniune  34196  sibfinima  34306  eulerpartlemt  34338  fiblem  34365  fibp1  34368  dstrvprob  34439  ballotlemsel1i  34480  ballotlemfrceq  34496  plymulx0  34514  signstfvc  34541  signstfveq0  34544  bnj944  34904  bnj998  34923  bnj1136  34963  bnj1408  35002  erdszelem4  35166  erdszelem8  35170  txsconnlem  35212  cvxsconn  35215  cvmliftpht  35290  snmlff  35301  elmrsubrn  35492  msrf  35514  mthmpps  35554  sinccvglem  35644  trer  36289  poimirlem6  37605  poimirlem7  37606  poimirlem9  37608  poimirlem17  37616  poimirlem20  37619  poimirlem28  37627  poimirlem29  37628  poimirlem30  37629  poimirlem31  37630  poimirlem32  37631  areacirc  37692  nnubfi  37729  prter1  38857  lkrlss  39073  diaf11N  41028  dibf11N  41140  lclkr  41512  lclkrs  41518  lcfrlem9  41529  lcfr  41564  mapd1o  41627  hdmapf1oN  41844  hgmapf1oN  41882  frlmvscadiccat  42479  fimgmcyc  42507  nacsfix  42685  eldioph2lem1  42733  irrapxlem1  42795  rmxypairf1o  42884  jm2.27a  42978  hbtlem2  43097  hbt  43103  mon1psubm  43172  onnog  43402  pren2d  43529  binomcxplemnotnn0  44329  elixpconstg  45067  elfzfzo  45259  monoords  45279  elfzod  45380  eluzd  45389  fmul01lt1lem2  45567  sumnnodd  45612  ioodvbdlimc1lem2  45914  ioodvbdlimc2lem  45916  iblsplit  45948  iblspltprt  45955  itgspltprt  45961  stoweidlem11  45993  stoweidlem17  45999  fourierdlem12  46101  fourierdlem20  46109  fourierdlem25  46114  fourierdlem37  46126  fourierdlem41  46130  fourierdlem48  46136  fourierdlem49  46137  fourierdlem50  46138  fourierdlem54  46142  fourierdlem64  46152  fourierdlem73  46161  fourierdlem79  46167  fourierdlem102  46190  fourierdlem111  46199  fourierdlem114  46202  etransclem23  46239  etransclem48  46264  ormkglobd  46857  2elfz2melfz  47303  elfzlble  47305  ceilhalfelfzo1  47315  1elfzo1ceilhalf1  47322  difltmodne  47327  modm2nep1  47351  modm1nep2  47353  modm1p1ne  47355  iccpartiltu  47407  iccpartigtl  47408  iccpartlt  47409  iccpartgt  47412  lswn0  47429  fmtnoge3  47515  fmtnodvds  47529  odz2prm2pw  47548  fmtnole4prm  47563  lighneallem4b  47594  mogoldbb  47770  nnsum4primesevenALTV  47786  bgoldbtbndlem3  47792  gpgprismgriedgdmss  48037  gpgprismgrusgra  48043  gpg3nbgrvtx0  48061  gpg3nbgrvtx0ALT  48062  gpg5nbgrvtx03star  48065  gpg5nbgr3star  48066  gpg3kgrtriexlem3  48070  gpg3kgrtriexlem4  48071  gpg3kgrtriexlem6  48073  gpgprismgr4cycllem3  48082  gpgprismgr4cycllem9  48088  ssnn0ssfz  48334  lmod1  48478  elfzolborelfzop1  48505  nnolog2flm1  48576  funcf2lem2  49068  isnatd  49209