Theorem syl3anbrc 1362

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  soisores  7332  limuni3  7852  onfununi  8334  smores2  8347  smoiso  8355  oelimcl  8592  iserd  8727  resixp  8944  undifixp  8945  alephval3  10117  canthwelem  10663  canthwe  10664  r1limwun  10749  wunex2  10751  tskcard  10794  gruina  10831  eluzmn  12898  eluzuzle  12900  uztrn  12909  eluzadd  12920  eluzsub  12921  subeluzsub  12924  nn0pzuz  12958  zsupss  12990  nn0ge2m1nnALT  12995  xov1plusxeqvd  13555  ige2m1fz  13676  0elfz  13683  uzsubfz0  13695  elfzmlbm  13697  difelfzle  13700  difelfznle  13701  fvffz0  13705  elfzod  13722  elfzolt2b  13730  elfzolt3b  13731  elfzouz2  13734  fzossrbm1  13748  elfzo0  13760  eluzgtdifelfzo  13787  elfzodifsumelfzo  13791  fzonn0p1  13802  fzonn0p1p1  13804  fzo0sn0fzo1  13815  ssfzo12bi  13821  fzoopth  13822  ubmelm1fzo  13823  elfzonelfzo  13829  fzosplitprm1  13838  fzostep1  13846  fvinim0ffz  13849  flword2  13878  uzsup  13928  modfzo0difsn  14011  modsumfzodifsn  14012  fsuppmapnn0fiub  14059  suppssfz  14062  1elfz0hash  14458  fzsdom2  14497  ccatdmss  14651  ccatrn  14659  ccat2s1fvw  14710  pfxn0  14760  pfxtrcfv0  14767  pfxtrcfvl  14770  swrdswrd  14778  swrdccatin1  14798  pfxccat3  14807  pfxccat3a  14811  repswswrd  14859  cshwidxmod  14878  cshw1  14897  cshwcsh2id  14903  swrds2  15015  pfx2  15022  2swrd2eqwrdeq  15030  ccat2s1fvwALT  15032  rexuzre  15444  limsupgre  15572  rlimclim1  15636  rlimclim  15637  climrlim2  15638  isercolllem1  15756  isercoll  15759  climcndslem1  15942  fallfacval4  16135  tanhbnd  16255  sinbnd2  16276  cosbnd2  16277  rpnnen2lem12  16319  nn0o  16479  bitsfzolem  16530  bitsfzo  16531  bitsmod  16532  bitsfi  16533  bitsinv1lem  16537  bitsinv1  16538  smueqlem  16586  dvdsnprmd  16786  2mulprm  16789  hashgcdlem  16885  prm23lt5  16912  zgz  17031  gznegcl  17033  gzcjcl  17034  gzaddcl  17035  gzmulcl  17036  vdwlem9  17087  prmgaplem3  17151  prmgaplem4  17152  cshwshashlem2  17194  setsstruct2  17272  ismred  17692  isfuncd  17960  homdmcoa  18162  isdrs2  18400  fpwipodrs  18634  ipodrsima  18635  chnub  18716  chnso  18718  sgrp2rid2ex  19045  subgid  19257  issubg2  19271  subsubg  19279  gaorber  19441  orbsta  19446  pmtrfconj  19599  psgnunilem2  19628  psgnunilem3  19629  psgnunilem4  19630  pgpfi1  19728  subgpgp  19730  pgpssslw  19747  subgslw  19749  sylow2alem2  19751  fislw  19758  sylow3lem3  19762  efgs1  19868  efgsp1  19870  efgsres  19871  efgredleme  19876  efgcpbllemb  19888  lt6abl  20028  telgsumfzs  20122  ablfac1eu  20208  submomnd  20265  isrngd  20314  prdsrngd  20317  ringrng  20432  isringrng  20434  isringd  20439  ringsrg  20445  ring1  20458  prdsringd  20467  subrngid  20717  subrngsubg  20720  issubrng2  20726  subsubrng  20731  subrgsubg  20745  subrgsubrng  20746  sdrgid  20964  cntzsdrg  20974  subdrgint  20975  sdrgint  20976  suborng  21048  islmodd  21056  islssd  21125  islss4  21152  dflidl2rng  21412  rnglidl0  21424  rnglidl1  21427  unichnlidl  21431  rnglidlrng  21450  rng2idlsubrng  21473  rhmpreimaidl  21485  ssdifidllem  21553  gzrngunit  21652  expmhm  21655  zringunit  21685  prmirredlem  21691  znidomb  21780  isphld  21873  ocvocv  21890  ocvlss  21891  frlmlbs  22016  psdmul  22400  gsummoncoe1  22539  mp2pm2mplem4  23040  chfacfisf  23085  chfacfisfcpmat  23086  chfacfscmulfsupp  23090  chfacfpmmulfsupp  23094  chfacfpmmulgsum2  23096  2ndcctbss  23687  finlocfin  23752  dissnlocfin  23761  locfindis  23762  locfincf  23763  isfild  24090  infil  24095  neifil  24112  flimfcls  24258  istgp2  24323  oppgtmd  24329  oppgtgp  24330  distgp  24331  indistgp  24332  efmndtmd  24333  submtmd  24336  subgtgp  24337  symgtgp  24338  qustgplem  24353  prdstmdd  24356  prdstgpd  24357  tlmtgp  24428  isngp4  24844  subgngp  24867  ngptgp  24868  tngngp2  24884  nrgtrg  24922  nrgtdrg  24925  elii2  25170  icopnfcnv  25176  xrhmeo  25180  lebnumii  25200  phtpcer  25229  reparpht  25232  phtpcco2  25233  pcohtpy  25254  pcoass  25258  pcorevlem  25260  isclmi  25311  isncvsngpd  25384  cphsubrglem  25411  cphclm  25423  phclm  25466  tcphcph  25471  clsocv  25484  cphsscph  25485  cmslssbn  25606  pjthlem2  25672  ovolf  25716  iundisj2  25783  vitalilem2  25843  vitali  25847  itg2monolem3  25986  dvfsumlem1  26260  dvfsumlem3  26262  mon1puc1p  26383  uc1pmon1p  26384  mon1pid  26386  ply1remlem  26397  drnguc1p  26406  plyaddlem1  26446  coeidlem  26470  plyn0mulidp  26518  aannenlem2  26572  radcnvcl  26660  pilem2  26695  coseq00topi  26747  coseq0negpitopi  26748  tangtx  26750  tanabsge  26751  cosq14gt0  26755  cosq14ge0  26756  cosq34lt1  26772  cosordlem  26775  cos0pilt1  26777  sinord  26779  resinf1o  26781  tanord1  26782  tanord  26783  efif1olem3  26789  efsubm  26796  relogrn  26806  logimclad  26817  logrnaddcl  26819  logneg  26833  logcj  26851  argregt0  26855  argrege0  26856  argimgt0  26857  argimlt0  26858  logimul  26859  logneg2  26860  logdmnrp  26886  logcnlem4  26890  dvloglem  26893  logf1o2  26895  efopnlem2  26902  cxpsqrtlem  26947  relogbval  27017  nnlogbexp  27026  relogbcxp  27030  relogbcxpb  27032  logbgt0b  27038  asinneg  27131  asinsin  27137  acoscos  27138  acosbnd  27145  atancj  27155  atanlogaddlem  27158  atanlogsublem  27160  atanlogsub  27161  atantan  27168  atanbndlem  27170  atans2  27176  leibpi  27187  scvxcvx  27230  jensenlem2  27232  emcllem7  27246  basellem1  27325  ppisval  27348  chtdif  27402  ppidif  27407  ppiub  27448  chtublem  27455  chtub  27456  lgsdilem2  27577  gausslemma2dlem1a  27609  gausslemma2dlem2  27611  gausslemma2dlem5  27615  gausslemma2dlem6  27616  lgsquadlem1  27624  lgsquadlem2  27625  lgsquadlem3  27626  2lgslem1  27638  2sqlem3  27664  chebbnd1lem1  27713  chebbnd1lem2  27714  chebbnd1lem3  27715  dchrisumlem2  27734  dchrvmasumlem2  27742  dchrvmasumiflem1  27745  dchrisum0flblem2  27753  mulog2sumlem2  27779  logdivbnd  27800  pntpbnd2  27831  pntibndlem1  27833  pntibnd  27837  pntlemc  27839  pntlemg  27842  pntlemq  27845  pntlemf  27849  padicabvf  27875  padicabvcxp  27876  ostth2  27881  noextend  27910  noextendseq  27911  nosupno  27947  noinfno  27962  ttgcontlem1  29349  axpaschlem  29405  nbgr2vtx1edg  29818  nbuhgr2vtx1edgb  29820  cusgrexi  29911  structtocusgr  29914  pthdadjvtx  30200  pthdlem1  30239  pthd  30242  crctcshwlkn0lem3  30288  crctcshwlkn0lem4  30289  crctcshwlkn0lem5  30290  crctcshwlkn0lem7  30292  wlkiswwlks1  30343  wwlksm1edg  30357  wwlksnred  30368  wwlksnredwwlkn  30371  wwlksnextproplem3  30387  clwlkclwwlklem2fv1  30473  clwlkclwwlklem2fv2  30474  clwlkclwwlklem2a  30476  clwlkclwwlklem2  30478  clwwisshclwwslemlem  30491  clwwisshclwwslem  30492  erclwwlkref  30498  clwwlkel  30524  clwwlkf  30525  wwlksext2clwwlk  30535  wwlksubclwwlk  30536  umgr2cwwkdifex  30543  1pthd  30621  eucrctshift  30731  dlwwlknondlwlknonf1olem1  30852  numclwlk2lem2f  30865  frgrreggt1  30881  grpoinvf  31021  strlem3a  32741  hstrlem3a  32749  iundisj2f  33071  fcoinver  33085  fresf1o  33112  ssnnssfz  33266  bcm1n  33274  iundisj2fi  33276  fsumrp0cl  33469  cycpmco2lem6  33579  fxpsdrg  33623  lmodslmd  33652  fldgensdrg  33763  intlidl  33856  idlinsubrg  33867  rhmimaidl  33868  ssmxidllem  33884  dflringlem2  33913  1arithidomlem1  33953  1arithidomlem2  33954  1arithidom  33955  fldextsdrg  34172  fldextrspunlem2  34195  fldextrspundgdvdslem  34198  fldextrspundgdvds  34199  minplyirred  34229  algextdeglem4  34238  algextdeglem8  34242  rtelextdg2lem  34244  constrsdrg  34293  2sqr3minply  34298  cos9thpiminply  34306  locfinreflem  34358  locfinref  34359  xrge0iifcnv  34451  xrge0iifiso  34453  xrge0iifhom  34455  esumc  34569  esumle  34576  esumlef  34580  esumpinfsum  34595  esumpcvgval  34596  fiunelros  34693  voliune  34748  volfiniune  34749  sibfinima  34858  eulerpartlemt  34890  fiblem  34917  fibp1  34920  dstrvprob  34991  ballotlemsel1i  35032  ballotlemfrceq  35048  signstfvc  35090  signstfveq0  35093  bnj944  35455  bnj998  35474  bnj1136  35514  bnj1408  35553  erdszelem4  35781  erdszelem8  35785  txsconnlem  35827  cvxsconn  35830  cvmliftpht  35905  snmlff  35916  elmrsubrn  36107  msrf  36129  mthmpps  36169  sinccvglem  36259  trer  36943  poimirlem6  38383  poimirlem7  38384  poimirlem9  38386  poimirlem17  38394  poimirlem20  38397  poimirlem28  38405  poimirlem29  38406  poimirlem30  38407  poimirlem31  38408  poimirlem32  38409  areacirc  38470  nnubfi  38508  prter1  39760  lkrlss  39976  diaf11N  41930  dibf11N  42042  lclkr  42414  lclkrs  42420  lcfrlem9  42431  lcfr  42466  mapd1o  42529  hdmapf1oN  42746  hgmapf1oN  42784  frlmvscadiccat  43402  fimgmcyc  43424  nacsfix  43565  eldioph2lem1  43613  irrapxlem1  43671  rmxypairf1o  43760  jm2.27a  43854  hbtlem2  43973  hbt  43979  mon1psubm  44048  onnoxpg  44277  pren2d  44404  binomcxplemnotnn0  45188  elixpconstg  45929  elfzfzo  46118  monoords  46138  eluzd  46245  fmul01lt1lem2  46423  sumnnodd  46468  ioodvbdlimc1lem2  46768  ioodvbdlimc2lem  46770  iblsplit  46802  iblspltprt  46809  itgspltprt  46815  stoweidlem11  46847  stoweidlem17  46853  fourierdlem12  46955  fourierdlem20  46963  fourierdlem25  46968  fourierdlem37  46980  fourierdlem41  46984  fourierdlem48  46990  fourierdlem50  46992  fourierdlem54  46996  fourierdlem64  47006  fourierdlem73  47015  fourierdlem79  47021  fourierdlem102  47044  fourierdlem111  47053  fourierdlem114  47056  etransclem23  47093  etransclem48  47118  ormkglobd  47713  chnsubseq  47716  2elfz2melfz  48214  elfzlble  48216  ceilhalfelfzo1  48230  1elfzo1ceilhalf1  48237  difltmodne  48244  modm2nep1  48268  modm1nep2  48270  modm1p1ne  48272  iccpartiltu  48330  iccpartigtl  48331  iccpartlt  48332  iccpartgt  48335  lswn0  48352  fmtnoge3  48441  fmtnodvds  48455  odz2prm2pw  48474  fmtnole4prm  48489  lighneallem4b  48520  nprmdvdsfacm1lem3  48533  nprmdvdsfacm1lem4  48534  nprmdvdsfacm1  48535  mogoldbb  48709  nnsum4primesevenALTV  48725  bgoldbtbndlem3  48731  gpgprismgriedgdmss  48976  gpgprismgrusgra  48982  gpg3nbgrvtx0  49000  gpg3nbgrvtx0ALT  49001  gpg5nbgrvtx03star  49004  gpg5nbgr3star  49005  gpg3kgrtriexlem3  49009  gpg3kgrtriexlem4  49010  gpg3kgrtriexlem6  49012  gpgprismgr4cycllem3  49021  gpgprismgr4cycllem9  49027  ssnn0ssfz  49287  lmod1  49430  elfzolborelfzop1  49457  nnolog2flm1  49528  funcf2lem2  50016  isnatd  50157