Theorem syl3anbrc 1246

Description: Syllogism inference. (Contributed by Mario Carneiro, 11-May-2014.)

Hypotheses

Ref	Expression
syl3anbrc.1	|- ( ph -> ps )
syl3anbrc.2	|- ( ph -> ch )
syl3anbrc.3	|- ( ph -> th )
syl3anbrc.4	|- ( ta <-> ( ps /\ ch /\ th ) )

Assertion

Ref	Expression
syl3anbrc	|- ( ph -> ta )

Proof of Theorem syl3anbrc

Step	Hyp	Ref	Expression
1		syl3anbrc.1	. . 3 |- ( ph -> ps )
2		syl3anbrc.2	. . 3 |- ( ph -> ch )
3		syl3anbrc.3	. . 3 |- ( ph -> th )
4	1, 2, 3	3jca 1242	. 2 |- ( ph -> ( ps /\ ch /\ th ) )
5		syl3anbrc.4	. 2 |- ( ta <-> ( ps /\ ch /\ th ) )
6	4, 5	sylibr 224	1 |- ( ph -> ta )

Syntax hints:   -> wi 4   <-> wb 196   /\ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  soisores  6577  limuni3  7052  onfununi  7438  smores2  7451  smoiso  7459  oelimcl  7680  iserd  7768  erinxp  7821  resixp  7943  undifixp  7944  alephval3  8933  fpwwe2lem12  9463  canthwelem  9472  canthwe  9473  r1limwun  9558  wunex2  9560  tskcard  9603  gruina  9640  nqerf  9752  nqerid  9755  eluzmn  11694  eluzuzle  11696  uztrn  11704  nn0pzuz  11745  zsupss  11777  nn0ge2m1nnALT  11782  xov1plusxeqvd  12318  ssfzunsnext  12386  ige2m1fz  12430  0elfz  12436  uzsubfz0  12447  elfzmlbm  12449  difelfzle  12452  difelfznle  12453  fvffz0  12457  elfzolt2b  12481  elfzolt3b  12482  elfzouz2  12484  fzossrbm1  12497  elfzo0  12508  eluzgtdifelfzo  12529  elfzodifsumelfzo  12533  fzonn0p1  12544  fzonn0p1p1  12546  elfzom1p1elfzo  12547  fzo0sn0fzo1  12557  ssfzo12bi  12563  ubmelm1fzo  12564  elfzonelfzo  12570  fzosplitprm1  12578  fzostep1  12584  fvinim0ffz  12587  flword2  12614  uzsup  12662  modfzo0difsn  12742  modsumfzodifsn  12743  fsuppmapnn0fiub  12790  fsuppmapnn0fiubOLD  12791  suppssfz  12794  1elfz0hash  13179  fzsdom2  13215  ccatrn  13372  swrdn0  13430  swrdtrcfv  13441  swrdtrcfv0  13442  swrdeq  13444  swrdtrcfvl  13450  swrdswrd  13460  swrdccatwrd  13468  wrdeqs1cat  13474  swrdccatin1  13483  swrdccat3  13492  swrdccatid  13497  repswswrd  13531  cshwidxmod  13549  cshw1  13568  cshwcsh2id  13574  swrds2  13685  2swrd2eqwrdeq  13696  ccat2s1fvwALT  13698  rexuzre  14092  limsupgre  14212  rlimclim1  14276  rlimclim  14277  climrlim2  14278  isercolllem1  14395  isercoll  14398  climcndslem1  14581  fallfacval4  14774  tanhbnd  14891  sinbnd2  14912  cosbnd2  14913  rpnnen2lem12  14954  nn0o  15099  bitsfzolem  15156  bitsfzo  15157  bitsmod  15158  bitsfi  15159  bitsinv1lem  15163  bitsinv1  15164  smueqlem  15212  dvdsnprmd  15403  hashgcdlem  15493  prm23lt5  15519  zgz  15637  gznegcl  15639  gzcjcl  15640  gzaddcl  15641  gzmulcl  15642  vdwlem9  15693  prmgaplem3  15757  prmgaplem4  15758  cshwshashlem2  15803  setsstruct2  15896  ismred  16262  isfuncd  16525  homdmcoa  16717  isdrs2  16939  fpwipodrs  17164  ipodrsima  17165  psss  17214  psssdm2  17215  sgrp2rid2ex  17414  subgid  17596  issubg2  17609  subsubg  17617  gaorber  17741  orbsta  17746  pmtrfconj  17886  psgnunilem2  17915  psgnunilem3  17916  psgnunilem4  17917  pgpfi1  18010  subgpgp  18012  pgpssslw  18029  subgslw  18031  sylow2alem2  18033  fislw  18040  sylow3lem3  18044  efgs1  18148  efgsp1  18150  efgsres  18151  efgredleme  18156  efgcpbllemb  18168  lt6abl  18296  telgsumfzs  18386  ablfac1eu  18472  isringd  18585  ringsrg  18589  ring1  18602  prdsringd  18612  subrgsubg  18786  islmodd  18869  islssd  18936  islss4  18962  gsummoncoe1  19674  gzrngunit  19812  expmhm  19815  zringunit  19836  prmirredlem  19841  znidomb  19910  isphld  19999  ocvocv  20015  ocvlss  20016  frlmlbs  20136  mp2pm2mplem4  20614  chfacfisf  20659  chfacfisfcpmat  20660  chfacfscmulfsupp  20664  chfacfpmmulfsupp  20668  chfacfpmmulgsum2  20670  2ndcctbss  21258  finlocfin  21323  dissnlocfin  21332  locfindis  21333  locfincf  21334  isfild  21662  infil  21667  neifil  21684  flimfcls  21830  istgp2  21895  oppgtmd  21901  oppgtgp  21902  distgp  21903  indistgp  21904  symgtgp  21905  submtmd  21908  subgtgp  21909  qustgplem  21924  prdstmdd  21927  prdstgpd  21928  tlmtgp  21999  isngp4  22416  subgngp  22439  ngptgp  22440  tngngp2  22456  nrgtrg  22494  nrgtdrg  22497  elii2  22735  icopnfcnv  22741  xrhmeo  22745  lebnumii  22765  phtpcer  22794  phtpcerOLD  22795  reparpht  22798  phtpcco2  22799  pcohtpy  22820  pcoass  22824  pcorevlem  22826  pi1cpbl  22844  pi1grplem  22849  isclmi  22877  isncvsngpd  22950  cphsubrglem  22977  cphclm  22989  tchclm  23031  tchcph  23036  clsocv  23049  pjthlem2  23209  ovolf  23250  iundisj2  23317  vitalilem2  23378  vitali  23382  itg2monolem3  23519  dvfsumlem1  23789  dvfsumlem3  23791  mon1puc1p  23910  uc1pmon1p  23911  ply1remlem  23922  drnguc1p  23930  plyaddlem1  23969  coeidlem  23993  aannenlem2  24084  radcnvcl  24171  pilem2  24206  coseq00topi  24254  coseq0negpitopi  24255  tangtx  24257  tanabsge  24258  cosq14gt0  24262  cosq14ge0  24263  cosordlem  24277  sinord  24280  resinf1o  24282  tanord1  24283  tanord  24284  efif1olem3  24290  efsubm  24297  relogrn  24308  logimclad  24319  logrnaddcl  24321  logneg  24334  logcj  24352  argregt0  24356  argrege0  24357  argimgt0  24358  argimlt0  24359  logimul  24360  logneg2  24361  logdmnrp  24387  logcnlem4  24391  dvloglem  24394  logf1o2  24396  efopnlem2  24403  cxpsqrtlem  24448  relogbval  24510  nnlogbexp  24519  relogbcxp  24523  relogbcxpb  24525  asinneg  24613  asinsin  24619  acoscos  24620  acosbnd  24627  atancj  24637  atanlogaddlem  24640  atanlogsublem  24642  atanlogsub  24643  atantan  24650  atanbndlem  24652  atans2  24658  leibpi  24669  scvxcvx  24712  jensenlem2  24714  emcllem7  24728  basellem1  24807  ppisval  24830  chtdif  24884  ppidif  24889  ppiub  24929  chtublem  24936  chtub  24937  lgsdilem2  25058  gausslemma2dlem1a  25090  gausslemma2dlem2  25092  gausslemma2dlem5  25096  gausslemma2dlem6  25097  lgsquadlem1  25105  lgsquadlem2  25106  lgsquadlem3  25107  2lgslem1  25119  2sqlem3  25145  chebbnd1lem1  25158  chebbnd1lem2  25159  chebbnd1lem3  25160  dchrisumlem2  25179  dchrvmasumlem2  25187  dchrvmasumiflem1  25190  dchrisum0flblem2  25198  mulog2sumlem2  25224  logdivbnd  25245  pntpbnd2  25276  pntibndlem1  25278  pntibnd  25282  pntlemc  25284  pntlemg  25287  pntlemq  25290  pntlemf  25294  padicabvf  25320  padicabvcxp  25321  ostth2  25326  ttgcontlem1  25765  axpaschlem  25820  pthdadjvtx  26626  pthdlem1  26662  pthd  26665  crctcshwlkn0lem3  26704  crctcshwlkn0lem4  26705  crctcshwlkn0lem5  26706  crctcshwlkn0lem7  26708  wlkiswwlks1  26753  wwlksm1edg  26767  wwlksnred  26787  wwlksnredwwlkn  26790  wwlksnextproplem3  26806  clwlkclwwlklem2fv1  26896  clwlkclwwlklem2fv2  26897  clwlkclwwlklem2a  26899  clwlkclwwlklem2  26901  clwwlksel  26914  clwwlksf  26915  wwlksext2clwwlk  26924  wwlksubclwwlks  26925  clwwisshclwwslemlem  26926  clwwisshclwwslem  26927  erclwwlksref  26934  umgr2cwwkdifex  26942  clwlksfclwwlk  26962  1pthd  27003  eucrctshift  27103  numclwlk2lem2f  27236  frgrreggt1  27251  grpoinvf  27386  strlem3a  29111  hstrlem3a  29119  iundisj2f  29403  fcoinver  29418  ssnnssfz  29549  bcm1n  29554  iundisj2fi  29556  fsumrp0cl  29695  submomnd  29710  lmodslmd  29757  suborng  29815  locfinreflem  29907  locfinref  29908  xrge0iifcnv  29979  xrge0iifiso  29981  xrge0iifhom  29983  esumc  30113  esumle  30120  esumlef  30124  esumpinfsum  30139  esumpcvgval  30140  fiunelros  30237  voliune  30292  volfiniune  30293  sibfinima  30401  eulerpartlemt  30433  fiblem  30460  fibp1  30463  dstrvprob  30533  ballotlemsel1i  30574  ballotlemfrceq  30590  plymulx0  30624  signstfvc  30651  signstfveq0  30654  bnj944  31008  bnj998  31026  bnj1136  31065  bnj1408  31104  erdszelem4  31176  erdszelem8  31180  txsconnlem  31222  cvxsconn  31225  cvmliftpht  31300  snmlff  31311  elmrsubrn  31417  msrf  31439  mthmpps  31479  sinccvglem  31566  noextend  31819  noextendseq  31820  nosupno  31849  trer  32310  poimirlem6  33415  poimirlem7  33416  poimirlem9  33418  poimirlem17  33426  poimirlem20  33429  poimirlem28  33437  poimirlem29  33438  poimirlem30  33439  poimirlem31  33440  poimirlem32  33441  areacirc  33505  nnubfi  33546  prter1  34164  lkrlss  34382  diaf11N  36338  dibf11N  36450  lclkr  36822  lclkrs  36828  lcfrlem9  36839  lcfr  36874  mapd1o  36937  hdmapf1oN  37157  hgmapf1oN  37195  nacsfix  37275  eldioph2lem1  37323  irrapxlem1  37386  rmxypairf1o  37476  jm2.27a  37572  hbtlem2  37694  hbt  37700  cntzsdrg  37772  mon1pid  37783  mon1psubm  37784  binomcxplemnotnn0  38555  elfzfzo  39488  monoords  39511  elfzod  39624  eluzd  39635  fmul01lt1lem2  39817  sumnnodd  39862  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  iblsplit  40182  iblspltprt  40189  itgspltprt  40195  stoweidlem11  40228  stoweidlem17  40234  fourierdlem12  40336  fourierdlem20  40344  fourierdlem25  40349  fourierdlem37  40361  fourierdlem41  40365  fourierdlem48  40371  fourierdlem49  40372  fourierdlem50  40373  fourierdlem54  40377  fourierdlem64  40387  fourierdlem73  40396  fourierdlem79  40402  fourierdlem102  40425  fourierdlem111  40434  fourierdlem114  40437  etransclem23  40474  etransclem48  40499  2elfz2melfz  41328  elfzlble  41330  fzoopth  41337  iccpartiltu  41358  iccpartigtl  41359  iccpartlt  41360  iccpartgt  41363  lswn0  41380  pfxtrcfv0  41402  pfxeq  41404  pfxtrcfvl  41405  pfx2  41412  pfxccat3  41426  pfxccat3a  41429  fmtnoge3  41442  fmtnodvds  41456  odz2prm2pw  41475  fmtnole4prm  41490  lighneallem4b  41526  mogoldbb  41673  nnsum4primesevenALTV  41689  bgoldbtbndlem3  41695  ringrng  41879  isringrng  41881  lidlrng  41927  ssnn0ssfz  42127  lmod1  42281  elfzolborelfzop1  42309  nnolog2flm1  42384