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  7336  mpt3fvotd  7690  limuni3  7864  onfununi  8353  smores2  8366  smoiso  8374  oelimcl  8613  iserd  8748  resixp  8965  undifixp  8966  alephval3  10193  canthwelem  10739  canthwe  10740  r1limwun  10825  wunex2  10827  tskcard  10870  gruina  10907  eluzmn  12976  eluzuzle  12978  uztrn  12987  eluzadd  12998  eluzsub  12999  subeluzsub  13002  nn0pzuz  13036  zsupss  13068  nn0ge2m1nnALT  13073  xov1plusxeqvd  13633  ige2m1fz  13755  0elfz  13762  uzsubfz0  13774  elfzmlbm  13776  difelfzle  13779  difelfznle  13780  fvffz0  13784  elfzod  13801  elfzolt2b  13809  elfzolt3b  13810  elfzouz2  13813  fzossrbm1  13827  elfzo0  13839  eluzgtdifelfzo  13866  elfzodifsumelfzo  13870  fzonn0p1  13881  fzonn0p1p1  13883  fzo0sn0fzo1  13894  ssfzo12bi  13900  fzoopth  13901  ubmelm1fzo  13902  elfzonelfzo  13908  fzosplitprm1  13917  fzostep1  13925  fvinim0ffz  13928  flword2  13957  uzsup  14007  modfzo0difsn  14090  modsumfzodifsn  14091  fsuppmapnn0fiub  14138  suppssfz  14141  1elfz0hash  14538  fzsdom2  14577  ccatdmss  14731  ccatrn  14739  ccat2s1fvw  14791  pfxn0  14841  pfxtrcfv0  14848  pfxtrcfvl  14851  swrdswrd  14859  swrdccatin1  14879  pfxccat3  14888  pfxccat3a  14892  repswswrd  14940  cshwidxmod  14959  cshw1  14978  cshwcsh2id  14984  swrds2  15097  pfx2  15104  2swrd2eqwrdeq  15112  ccat2s1fvwALT  15114  rexuzre  15526  limsupgre  15654  rlimclim1  15718  rlimclim  15719  climrlim2  15720  isercolllem1  15838  isercoll  15841  climcndslem1  16024  fallfacval4  16215  tanhbnd  16335  sinbnd2  16356  cosbnd2  16357  rpnnen2lem12  16399  nn0o  16559  bitsfzolem  16610  bitsfzo  16611  bitsmod  16612  bitsfi  16613  bitsinv1lem  16617  bitsinv1  16618  smueqlem  16666  dvdsnprmd  16871  2mulprm  16874  hashgcdlem  16971  prm23lt5  16998  zgz  17117  gznegcl  17119  gzcjcl  17120  gzaddcl  17121  gzmulcl  17122  vdwlem9  17173  prmgaplem3  17237  prmgaplem4  17238  cshwshashlem2  17280  setsstruct2  17358  ismred  17778  isfuncd  18046  homdmcoa  18248  isdrs2  18486  fpwipodrs  18720  ipodrsima  18721  chnub  18802  chnso  18804  sgrp2rid2ex  19132  subgid  19344  issubg2  19358  subsubg  19366  gaorber  19528  orbsta  19533  pmtrfconj  19686  psgnunilem2  19715  psgnunilem3  19716  psgnunilem4  19717  pgpfi1  19815  subgpgp  19817  pgpssslw  19834  subgslw  19836  sylow2alem2  19838  fislw  19845  sylow3lem3  19849  efgs1  19955  efgsp1  19957  efgsres  19958  efgredleme  19963  efgcpbllemb  19975  lt6abl  20115  telgsumfzs  20209  ablfac1eu  20295  submomnd  20352  isrngd  20401  prdsrngd  20404  ringrng  20520  isringrng  20522  isringd  20528  ringsrg  20534  ring1  20547  prdsringd  20556  subrngid  20807  subrngsubg  20810  issubrng2  20816  subsubrng  20821  subrgsubg  20835  subrgsubrng  20836  sdrgid  21055  cntzsdrg  21065  subdrgint  21066  sdrgint  21067  suborng  21139  islmodd  21147  islssd  21216  islss4  21243  dflidl2rng  21503  rnglidl0  21515  rnglidl1  21518  unichnlidl  21522  rnglidlrng  21541  rng2idlsubrng  21565  rhmpreimaidl  21577  ssdifidllem  21646  gzrngunit  21745  expmhm  21748  zringunit  21778  prmirredlem  21784  znidomb  21873  isphld  21966  ocvocv  21983  ocvlss  21984  frlmlbs  22109  psdmul  22493  gsummoncoe1  22632  mp2pm2mplem4  23133  chfacfisf  23178  chfacfisfcpmat  23179  chfacfscmulfsupp  23183  chfacfpmmulfsupp  23187  chfacfpmmulgsum2  23189  2ndcctbss  23780  finlocfin  23845  dissnlocfin  23854  locfindis  23855  locfincf  23856  isfild  24183  infil  24188  neifil  24205  flimfcls  24351  istgp2  24416  oppgtmd  24422  oppgtgp  24423  distgp  24424  indistgp  24425  efmndtmd  24426  submtmd  24429  subgtgp  24430  symgtgp  24431  qustgplem  24446  prdstmdd  24449  prdstgpd  24450  tlmtgp  24521  isngp4  24937  subgngp  24960  ngptgp  24961  tngngp2  24977  nrgtrg  25015  nrgtdrg  25018  elii2  25263  icopnfcnv  25269  xrhmeo  25273  lebnumii  25293  phtpcer  25322  reparpht  25325  phtpcco2  25326  pcohtpy  25347  pcoass  25351  pcorevlem  25353  isclmi  25404  isncvsngpd  25477  cphsubrglem  25504  cphclm  25516  phclm  25559  tcphcph  25564  clsocv  25577  cphsscph  25578  cmslssbn  25699  pjthlem2  25765  ovolf  25809  iundisj2  25876  vitalilem2  25936  vitali  25940  itg2monolem3  26079  dvfsumlem1  26352  dvfsumlem3  26354  mon1puc1p  26475  uc1pmon1p  26476  mon1pid  26478  ply1remlem  26489  drnguc1p  26498  plyaddlem1  26538  coeidlem  26562  plyn0mulidp  26608  aannenlem2  26662  radcnvcl  26750  pilem2  26785  coseq00topi  26837  coseq0negpitopi  26838  tangtx  26840  tanabsge  26841  cosq14gt0  26845  cosq14ge0  26846  cosq34lt1  26861  cosordlem  26864  cos0pilt1  26866  sinord  26868  resinf1o  26870  tanord1  26871  tanord  26872  efif1olem3  26878  efsubm  26885  relogrn  26895  logimclad  26906  logrnaddcl  26908  logneg  26922  logcj  26940  argregt0  26944  argrege0  26945  argimgt0  26946  argimlt0  26947  logimul  26948  logneg2  26949  logdmnrp  26975  logcnlem4  26979  dvloglem  26982  logf1o2  26984  efopnlem2  26991  cxpsqrtlem  27036  relogbval  27106  nnlogbexp  27115  relogbcxp  27119  relogbcxpb  27121  logbgt0b  27127  asinneg  27220  asinsin  27226  acoscos  27227  acosbnd  27234  atancj  27244  atanlogaddlem  27247  atanlogsublem  27249  atanlogsub  27250  atantan  27257  atanbndlem  27259  atans2  27265  leibpi  27276  scvxcvx  27319  jensenlem2  27321  emcllem7  27335  basellem1  27414  ppisval  27437  chtdif  27491  ppidif  27496  ppiub  27537  chtublem  27544  chtub  27545  lgsdilem2  27666  gausslemma2dlem1a  27698  gausslemma2dlem2  27700  gausslemma2dlem5  27704  gausslemma2dlem6  27705  lgsquadlem1  27713  lgsquadlem2  27714  lgsquadlem3  27715  2lgslem1  27727  2sqlem3  27753  chebbnd1lem1  27802  chebbnd1lem2  27803  chebbnd1lem3  27804  dchrisumlem2  27823  dchrvmasumlem2  27831  dchrvmasumiflem1  27834  dchrisum0flblem2  27842  mulog2sumlem2  27868  logdivbnd  27889  pntpbnd2  27920  pntibndlem1  27922  pntibnd  27926  pntlemc  27928  pntlemg  27931  pntlemq  27934  pntlemf  27938  padicabvf  27964  padicabvcxp  27965  ostth2  27970  fltoprmlem2  28000  noextend  28029  noextendseq  28030  nosupno  28066  noinfno  28081  ttgcontlem1  29468  axpaschlem  29524  nbgr2vtx1edg  29937  nbuhgr2vtx1edgb  29939  cusgrexi  30030  structtocusgr  30033  pthdadjvtx  30319  pthdlem1  30358  pthd  30361  crctcshwlkn0lem3  30407  crctcshwlkn0lem4  30408  crctcshwlkn0lem5  30409  crctcshwlkn0lem7  30411  wlkiswwlks1  30462  wwlksm1edg  30476  wwlksnred  30487  wwlksnredwwlkn  30490  wwlksnextproplem3  30506  clwlkclwwlklem2fv1  30592  clwlkclwwlklem2fv2  30593  clwlkclwwlklem2a  30595  clwlkclwwlklem2  30597  clwwisshclwwslemlem  30610  clwwisshclwwslem  30611  erclwwlkref  30617  clwwlkel  30643  clwwlkf  30644  wwlksext2clwwlk  30654  wwlksubclwwlk  30655  umgr2cwwkdifex  30662  1pthd  30740  eucrctshift  30850  dlwwlknondlwlknonf1olem1  30971  numclwlk2lem2f  30984  frgrreggt1  31000  grpoinvf  31140  strlem3a  32860  hstrlem3a  32868  iundisj2f  33232  fcoinver  33246  fresf1o  33273  ssnnssfz  33426  bcm1n  33434  iundisj2fi  33436  fsumrp0cl  33629  cycpmco2lem6  33739  fxpsdrg  33783  lmodslmd  33812  fldgensdrg  33923  intlidl  34017  idlinsubrg  34028  rhmimaidl  34029  ssmxidllem  34045  dflringlem2  34074  1arithidomlem1  34114  1arithidomlem2  34115  1arithidom  34116  fldextsdrg  34333  fldextrspunlem2  34356  fldextrspundgdvdslem  34359  fldextrspundgdvds  34360  minplyirred  34390  algextdeglem4  34399  algextdeglem8  34403  rtelextdg2lem  34405  constrsdrg  34454  2sqr3minply  34459  cos9thpiminply  34467  locfinreflem  34519  locfinref  34520  xrge0iifcnv  34612  xrge0iifiso  34614  xrge0iifhom  34616  esumc  34730  esumle  34737  esumlef  34741  esumpinfsum  34756  esumpcvgval  34757  fiunelros  34854  voliune  34909  volfiniune  34910  sibfinima  35018  eulerpartlemt  35050  fiblem  35077  fibp1  35080  dstrvprob  35151  ballotlemsel1i  35192  ballotlemfrceq  35208  signstfvc  35250  signstfveq0  35253  bnj944  35615  bnj998  35634  bnj1136  35674  bnj1408  35713  erdszelem4  36046  erdszelem8  36050  txsconnlem  36092  cvxsconn  36095  cvmliftpht  36170  snmlff  36181  elmrsubrn  36372  msrf  36394  mthmpps  36434  sinccvglem  36524  trer  37197  poimirlem6  38638  poimirlem7  38639  poimirlem9  38641  poimirlem17  38649  poimirlem20  38652  poimirlem28  38660  poimirlem29  38661  poimirlem30  38662  poimirlem31  38663  poimirlem32  38664  areacirc  38725  nnubfi  38778  prter1  40030  lkrlss  40246  diaf11N  42200  dibf11N  42312  lclkr  42684  lclkrs  42690  lcfrlem9  42701  lcfr  42736  mapd1o  42799  hdmapf1oN  43016  hgmapf1oN  43054  frlmvscadiccat  43667  fimgmcyc  43692  nacsfix  43817  eldioph2lem1  43865  irrapxlem1  43923  rmxypairf1o  44012  jm2.27a  44106  hbtlem2  44220  hbt  44226  mon1psubm  44295  onnoxpg  44524  pren2d  44651  binomcxplemnotnn0  45434  elixpconstg  46198  elfzfzo  46387  monoords  46407  eluzd  46513  fmul01lt1lem2  46691  sumnnodd  46736  ioodvbdlimc1lem2  47036  ioodvbdlimc2lem  47038  iblsplit  47070  iblspltprt  47077  itgspltprt  47083  stoweidlem11  47115  stoweidlem17  47121  fourierdlem12  47223  fourierdlem20  47231  fourierdlem25  47236  fourierdlem37  47248  fourierdlem41  47252  fourierdlem48  47258  fourierdlem50  47260  fourierdlem54  47264  fourierdlem64  47274  fourierdlem73  47283  fourierdlem79  47289  fourierdlem102  47312  fourierdlem111  47321  fourierdlem114  47324  etransclem23  47361  etransclem48  47386  ormkglobd  47981  chnsubseq  47984  2elfz2melfz  48482  elfzlble  48484  ceilhalfelfzo1  48498  1elfzo1ceilhalf1  48505  difltmodne  48512  modm2nep1  48536  modm1nep2  48538  modm1p1ne  48540  iccpartiltu  48598  iccpartigtl  48599  iccpartlt  48600  iccpartgt  48603  lswn0  48620  fmtnoge3  48709  fmtnodvds  48723  odz2prm2pw  48742  fmtnole4prm  48757  lighneallem4b  48788  nprmdvdsfacm1lem3  48801  nprmdvdsfacm1lem4  48802  nprmdvdsfacm1  48803  mogoldbb  48977  nnsum4primesevenALTV  48993  bgoldbtbndlem3  48999  gpgprismgriedgdmss  49244  gpgprismgrusgra  49250  gpg3nbgrvtx0  49268  gpg3nbgrvtx0ALT  49269  gpg5nbgrvtx03star  49272  gpg5nbgr3star  49273  gpg3kgrtriexlem3  49277  gpg3kgrtriexlem4  49278  gpg3kgrtriexlem6  49280  gpgprismgr4cycllem3  49289  gpgprismgr4cycllem9  49295  ssnn0ssfz  49555  lmod1  49698  elfzolborelfzop1  49725  nnolog2flm1  49796  funcf2lem2  50290  isnatd  50433