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  7320  limuni3  7847  onfununi  8355  smores2  8368  smoiso  8376  oelimcl  8612  iserd  8745  resixp  8947  undifixp  8948  alephval3  10124  canthwelem  10664  canthwe  10665  r1limwun  10750  wunex2  10752  tskcard  10795  gruina  10832  eluzmn  12859  eluzuzle  12861  uztrn  12870  eluzadd  12881  eluzsub  12882  subeluzsub  12889  nn0pzuz  12921  zsupss  12953  nn0ge2m1nnALT  12958  xov1plusxeqvd  13515  ige2m1fz  13634  0elfz  13641  uzsubfz0  13653  elfzmlbm  13655  difelfzle  13658  difelfznle  13659  fvffz0  13663  elfzolt2b  13687  elfzolt3b  13688  elfzouz2  13691  fzossrbm1  13705  elfzo0  13717  eluzgtdifelfzo  13743  elfzodifsumelfzo  13747  fzonn0p1  13758  fzonn0p1p1  13760  fzo0sn0fzo1  13771  ssfzo12bi  13777  fzoopth  13778  ubmelm1fzo  13779  elfzonelfzo  13785  fzosplitprm1  13793  fzostep1  13799  fvinim0ffz  13802  flword2  13830  uzsup  13880  modfzo0difsn  13961  modsumfzodifsn  13962  fsuppmapnn0fiub  14009  suppssfz  14012  1elfz0hash  14408  fzsdom2  14446  ccatrn  14607  ccat2s1fvw  14656  pfxn0  14704  pfxtrcfv0  14712  pfxtrcfvl  14715  swrdswrd  14723  swrdccatin1  14743  pfxccat3  14752  pfxccat3a  14756  repswswrd  14802  cshwidxmod  14821  cshw1  14840  cshwcsh2id  14847  swrds2  14959  pfx2  14966  2swrd2eqwrdeq  14972  ccat2s1fvwALT  14974  rexuzre  15371  limsupgre  15497  rlimclim1  15561  rlimclim  15562  climrlim2  15563  isercolllem1  15681  isercoll  15684  climcndslem1  15865  fallfacval4  16059  tanhbnd  16179  sinbnd2  16200  cosbnd2  16201  rpnnen2lem12  16243  nn0o  16402  bitsfzolem  16453  bitsfzo  16454  bitsmod  16455  bitsfi  16456  bitsinv1lem  16460  bitsinv1  16461  smueqlem  16509  dvdsnprmd  16709  2mulprm  16712  hashgcdlem  16807  prm23lt5  16834  zgz  16953  gznegcl  16955  gzcjcl  16956  gzaddcl  16957  gzmulcl  16958  vdwlem9  17009  prmgaplem3  17073  prmgaplem4  17074  cshwshashlem2  17116  setsstruct2  17193  ismred  17614  isfuncd  17878  homdmcoa  18080  isdrs2  18318  fpwipodrs  18550  ipodrsima  18551  sgrp2rid2ex  18905  subgid  19111  issubg2  19124  subsubg  19132  gaorber  19291  orbsta  19296  pmtrfconj  19447  psgnunilem2  19476  psgnunilem3  19477  psgnunilem4  19478  pgpfi1  19576  subgpgp  19578  pgpssslw  19595  subgslw  19597  sylow2alem2  19599  fislw  19606  sylow3lem3  19610  efgs1  19716  efgsp1  19718  efgsres  19719  efgredleme  19724  efgcpbllemb  19736  lt6abl  19876  telgsumfzs  19970  ablfac1eu  20056  isrngd  20133  prdsrngd  20136  ringrng  20245  isringrng  20247  isringd  20251  ringsrg  20257  ring1  20270  prdsringd  20281  subrngid  20509  subrngsubg  20512  issubrng2  20518  subsubrng  20523  subrgsubg  20537  subrgsubrng  20538  sdrgid  20752  cntzsdrg  20762  subdrgint  20763  sdrgint  20764  islmodd  20823  islssd  20892  islss4  20919  dflidl2rng  21179  rnglidl0  21190  rnglidl1  21193  rnglidlrng  21208  rng2idlsubrng  21226  rhmpreimaidl  21238  gzrngunit  21401  expmhm  21404  zringunit  21427  prmirredlem  21433  znidomb  21522  isphld  21614  ocvocv  21631  ocvlss  21632  frlmlbs  21757  psdmul  22104  gsummoncoe1  22246  mp2pm2mplem4  22747  chfacfisf  22792  chfacfisfcpmat  22793  chfacfscmulfsupp  22797  chfacfpmmulfsupp  22801  chfacfpmmulgsum2  22803  2ndcctbss  23393  finlocfin  23458  dissnlocfin  23467  locfindis  23468  locfincf  23469  isfild  23796  infil  23801  neifil  23818  flimfcls  23964  istgp2  24029  oppgtmd  24035  oppgtgp  24036  distgp  24037  indistgp  24038  efmndtmd  24039  submtmd  24042  subgtgp  24043  symgtgp  24044  qustgplem  24059  prdstmdd  24062  prdstgpd  24063  tlmtgp  24134  isngp4  24551  subgngp  24574  ngptgp  24575  tngngp2  24591  nrgtrg  24629  nrgtdrg  24632  elii2  24883  icopnfcnv  24891  xrhmeo  24895  lebnumii  24916  phtpcer  24945  reparpht  24949  phtpcco2  24950  pcohtpy  24971  pcoass  24975  pcorevlem  24977  isclmi  25028  isncvsngpd  25102  cphsubrglem  25129  cphclm  25141  phclm  25184  tcphcph  25189  clsocv  25202  cphsscph  25203  cmslssbn  25324  pjthlem2  25390  ovolf  25435  iundisj2  25502  vitalilem2  25562  vitali  25566  itg2monolem3  25705  dvfsumlem1  25984  dvfsumlem3  25987  mon1puc1p  26108  uc1pmon1p  26109  mon1pid  26111  ply1remlem  26122  drnguc1p  26131  plyaddlem1  26170  coeidlem  26194  aannenlem2  26289  radcnvcl  26378  pilem2  26414  coseq00topi  26463  coseq0negpitopi  26464  tangtx  26466  tanabsge  26467  cosq14gt0  26471  cosq14ge0  26472  cosq34lt1  26488  cosordlem  26491  cos0pilt1  26493  sinord  26495  resinf1o  26497  tanord1  26498  tanord  26499  efif1olem3  26505  efsubm  26512  relogrn  26522  logimclad  26533  logrnaddcl  26535  logneg  26549  logcj  26567  argregt0  26571  argrege0  26572  argimgt0  26573  argimlt0  26574  logimul  26575  logneg2  26576  logdmnrp  26602  logcnlem4  26606  dvloglem  26609  logf1o2  26611  efopnlem2  26618  cxpsqrtlem  26663  relogbval  26734  nnlogbexp  26743  relogbcxp  26747  relogbcxpb  26749  logbgt0b  26755  asinneg  26848  asinsin  26854  acoscos  26855  acosbnd  26862  atancj  26872  atanlogaddlem  26875  atanlogsublem  26877  atanlogsub  26878  atantan  26885  atanbndlem  26887  atans2  26893  leibpi  26904  scvxcvx  26948  jensenlem2  26950  emcllem7  26964  basellem1  27043  ppisval  27066  chtdif  27120  ppidif  27125  ppiub  27167  chtublem  27174  chtub  27175  lgsdilem2  27296  gausslemma2dlem1a  27328  gausslemma2dlem2  27330  gausslemma2dlem5  27334  gausslemma2dlem6  27335  lgsquadlem1  27343  lgsquadlem2  27344  lgsquadlem3  27345  2lgslem1  27357  2sqlem3  27383  chebbnd1lem1  27432  chebbnd1lem2  27433  chebbnd1lem3  27434  dchrisumlem2  27453  dchrvmasumlem2  27461  dchrvmasumiflem1  27464  dchrisum0flblem2  27472  mulog2sumlem2  27498  logdivbnd  27519  pntpbnd2  27550  pntibndlem1  27552  pntibnd  27556  pntlemc  27558  pntlemg  27561  pntlemq  27564  pntlemf  27568  padicabvf  27594  padicabvcxp  27595  ostth2  27600  noextend  27630  noextendseq  27631  nosupno  27667  noinfno  27682  ttgcontlem1  28864  axpaschlem  28919  nbgr2vtx1edg  29329  nbuhgr2vtx1edgb  29331  cusgrexi  29422  structtocusgr  29425  pthdadjvtx  29710  pthdlem1  29748  pthd  29751  crctcshwlkn0lem3  29794  crctcshwlkn0lem4  29795  crctcshwlkn0lem5  29796  crctcshwlkn0lem7  29798  wlkiswwlks1  29849  wwlksm1edg  29863  wwlksnred  29874  wwlksnredwwlkn  29877  wwlksnextproplem3  29893  clwlkclwwlklem2fv1  29976  clwlkclwwlklem2fv2  29977  clwlkclwwlklem2a  29979  clwlkclwwlklem2  29981  clwwisshclwwslemlem  29994  clwwisshclwwslem  29995  erclwwlkref  30001  clwwlkel  30027  clwwlkf  30028  wwlksext2clwwlk  30038  wwlksubclwwlk  30039  umgr2cwwkdifex  30046  1pthd  30124  eucrctshift  30224  dlwwlknondlwlknonf1olem1  30345  numclwlk2lem2f  30358  frgrreggt1  30374  grpoinvf  30513  strlem3a  32233  hstrlem3a  32241  iundisj2f  32571  fcoinver  32585  fresf1o  32609  ssnnssfz  32764  bcm1n  32772  iundisj2fi  32774  ccatdmss  32925  chnub  32992  chnso  32994  fsumrp0cl  33016  submomnd  33078  cycpmco2lem6  33142  lmodslmd  33201  fldgensdrg  33308  suborng  33337  intlidl  33435  idlinsubrg  33446  rhmimaidl  33447  ssdifidllem  33471  ssmxidllem  33488  1arithidomlem1  33550  1arithidomlem2  33551  1arithidom  33552  fldextsdrg  33696  fldextrspunlem2  33718  fldextrspundgdvdslem  33721  fldextrspundgdvds  33722  minplyirred  33745  algextdeglem4  33754  algextdeglem8  33758  rtelextdg2lem  33760  constrsdrg  33809  2sqr3minply  33814  cos9thpiminply  33822  locfinreflem  33871  locfinref  33872  xrge0iifcnv  33964  xrge0iifiso  33966  xrge0iifhom  33968  esumc  34082  esumle  34089  esumlef  34093  esumpinfsum  34108  esumpcvgval  34109  fiunelros  34205  voliune  34260  volfiniune  34261  sibfinima  34371  eulerpartlemt  34403  fiblem  34430  fibp1  34433  dstrvprob  34504  ballotlemsel1i  34545  ballotlemfrceq  34561  plymulx0  34579  signstfvc  34606  signstfveq0  34609  bnj944  34969  bnj998  34988  bnj1136  35028  bnj1408  35067  erdszelem4  35216  erdszelem8  35220  txsconnlem  35262  cvxsconn  35265  cvmliftpht  35340  snmlff  35351  elmrsubrn  35542  msrf  35564  mthmpps  35604  sinccvglem  35694  trer  36334  poimirlem6  37650  poimirlem7  37651  poimirlem9  37653  poimirlem17  37661  poimirlem20  37664  poimirlem28  37672  poimirlem29  37673  poimirlem30  37674  poimirlem31  37675  poimirlem32  37676  areacirc  37737  nnubfi  37774  prter1  38897  lkrlss  39113  diaf11N  41068  dibf11N  41180  lclkr  41552  lclkrs  41558  lcfrlem9  41569  lcfr  41604  mapd1o  41667  hdmapf1oN  41884  hgmapf1oN  41922  sn-inelr  42510  frlmvscadiccat  42529  fimgmcyc  42557  nacsfix  42735  eldioph2lem1  42783  irrapxlem1  42845  rmxypairf1o  42935  jm2.27a  43029  hbtlem2  43148  hbt  43154  mon1psubm  43223  onnog  43453  pren2d  43580  binomcxplemnotnn0  44380  elixpconstg  45113  elfzfzo  45305  monoords  45326  elfzod  45427  eluzd  45436  fmul01lt1lem2  45614  sumnnodd  45659  ioodvbdlimc1lem2  45961  ioodvbdlimc2lem  45963  iblsplit  45995  iblspltprt  46002  itgspltprt  46008  stoweidlem11  46040  stoweidlem17  46046  fourierdlem12  46148  fourierdlem20  46156  fourierdlem25  46161  fourierdlem37  46173  fourierdlem41  46177  fourierdlem48  46183  fourierdlem49  46184  fourierdlem50  46185  fourierdlem54  46189  fourierdlem64  46199  fourierdlem73  46208  fourierdlem79  46214  fourierdlem102  46237  fourierdlem111  46246  fourierdlem114  46249  etransclem23  46286  etransclem48  46311  ormkglobd  46904  2elfz2melfz  47347  elfzlble  47349  ceilhalfelfzo1  47359  1elfzo1ceilhalf1  47366  difltmodne  47371  iccpartiltu  47436  iccpartigtl  47437  iccpartlt  47438  iccpartgt  47441  lswn0  47458  fmtnoge3  47544  fmtnodvds  47558  odz2prm2pw  47577  fmtnole4prm  47592  lighneallem4b  47623  mogoldbb  47799  nnsum4primesevenALTV  47815  bgoldbtbndlem3  47821  grlimgrtrilem1  48006  gpgprismgriedgdmss  48056  gpgprismgrusgra  48062  gpg3nbgrvtx0  48078  gpg3nbgrvtx0ALT  48079  gpg5nbgrvtx03star  48082  gpg5nbgr3star  48083  gpg3kgrtriexlem3  48087  gpg3kgrtriexlem4  48088  gpg3kgrtriexlem6  48090  gpgprismgr4cycllem3  48096  gpgprismgr4cycllem9  48102  ssnn0ssfz  48324  lmod1  48468  elfzolborelfzop1  48495  nnolog2flm1  48570  funcf2lem2  49047  isnatd  49143