Theorem sylanbrc 417

Description: Syllogism inference. (Contributed by Jeff Madsen, 2-Sep-2009.)

Hypotheses

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

Assertion

Ref	Expression
sylanbrc	|- ( ph -> th )

Proof of Theorem sylanbrc

Step	Hyp	Ref	Expression
1		sylanbrc.1	. . 3 |- ( ph -> ps )
2		sylanbrc.2	. . 3 |- ( ph -> ch )
3	1, 2	jca 306	. 2 |- ( ph -> ( ps /\ ch ) )
4		sylanbrc.3	. 2 |- ( th <-> ( ps /\ ch ) )
5	3, 4	sylibr 134	1 |- ( ph -> th )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  dcand  941  ecase2d  1388  sb2  1816  sbequ1  1817  sbidm  1900  eqeu  2990  euind  3007  reuind  3025  eldifd  3224  eqssd  3259  ssrabdv  3321  elind  3408  dcun  3623  opm  4355  issod  4445  ordsucim  4627  onintonm  4644  ordtri2or2exmidlem  4653  en2lp  4681  ordwe  4703  sosng  4828  sotri2  5165  sotri3  5166  relssdmrn  5288  funun  5402  fnsng  5408  fnprg  5416  fntpg  5417  fntp  5418  fununi  5429  imain  5443  fnco  5471  f00  5564  f1ss  5584  f1ssr  5585  f1ssres  5587  f1f1orn  5630  foimacnv  5637  foun  5638  fun11iun  5640  sefvex  5696  dff3im  5827  fmpt  5832  ffnfv  5840  fmpt2d  5844  ffvresb  5845  fprg  5872  foco2  5932  fcof1  5962  fcofo  5963  fcof1o  5968  fliftf  5978  isoini2  5998  f1oiso  6005  moriotass  6042  fnoprabg  6162  f1ocnvd  6265  f1o3d  6271  suppssov1  6272  1stcof  6370  2ndcof  6371  1stconst  6430  2ndconst  6431  fo2ndf  6436  f1o2ndf1  6437  f1od2  6444  suppssfvg  6476  smores2  6538  tfrlem5  6558  tfrlemibfn  6572  tfr1onlembfn  6588  tfri1dALT  6595  tfrcllembfn  6601  nntri2  6740  eroveu  6873  elixpsn  6983  dom2lem  7024  xpf1o  7110  fidifsnen  7138  finexdc  7173  elssdc  7175  unfidisj  7195  f1finf1o  7230  fidcenumlemrks  7236  sbthlemi9  7248  supeuti  7298  infeuti  7333  casef1  7394  caseinl  7395  caseinr  7396  difinfsnlem  7403  ctmlemr  7412  ctm  7413  ctssdclemn0  7414  ctssdccl  7415  ctssdc  7417  enumctlemm  7418  nnnninf  7430  nninfwlpoimlemg  7479  en2other2  7512  exmidfodomrlemim  7517  pw1if  7548  pw1nel3  7554  dftap2  7581  cc2lem  7596  cc4f  7599  addclpi  7658  mulclpi  7659  nnppipi  7674  recmulnqg  7722  enq0ref  7764  nqnq0pi  7769  genipv  7840  addclpr  7868  nqprxx  7877  prmuloc  7897  mulclpr  7903  distrlem1prl  7913  distrlem1pru  7914  ltexprlempr  7939  ltexprlemrl  7941  ltexprlemru  7943  lteupri  7948  recexprlempr  7963  cauappcvgprlemm  7976  cauappcvgprlemopl  7977  cauappcvgprlemlol  7978  cauappcvgprlemopu  7979  cauappcvgprlemupu  7980  cauappcvgprlemloc  7983  cauappcvgprlemcl  7984  cauappcvgprlemladdfu  7985  cauappcvgprlemladdfl  7986  cauappcvgprlem2  7991  caucvgprlemm  7999  caucvgprlemopl  8000  caucvgprlemlol  8001  caucvgprlemopu  8002  caucvgprlemupu  8003  caucvgprlemloc  8006  caucvgprlemcl  8007  caucvgprlemladdfu  8008  caucvgprlem2  8011  caucvgprprlemml  8025  caucvgprprlemmu  8026  caucvgprprlemopl  8028  caucvgprprlemlol  8029  caucvgprprlemopu  8030  caucvgprprlemupu  8031  caucvgprprlemloc  8034  caucvgprprlemcl  8035  caucvgprprlem2  8041  suplocexprlemex  8053  suplocsrlem  8139  elrealeu  8160  rereceu  8220  axpre-suploclemres  8232  negf1o  8672  aptap  8941  receuap  8960  divvalap  8965  cju  9252  nn0ge2m1nn  9577  nnnegz  9597  elnnz  9604  elnn0z  9607  peano2z  9630  nn0n0n1ge2  9665  msqznn  9696  eluzaddi  9899  eluzsubi  9900  uzind4  9938  supinfneg  9945  infsupneg  9946  elnn1uz2  9957  uz2mulcl  9958  divfnzn  9971  nnrp  10014  rpaddcl  10028  rpmulcl  10029  rpdivcl  10030  rpgecl  10033  ge0p1rp  10036  elrpd  10044  ge0addcl  10333  ge0mulcl  10334  ge0xaddcl  10335  icoshftf1o  10343  peano2fzr  10391  uzsubsubfz  10401  fzsplit2  10404  fzsplit3  10407  elfznn  10409  fzss1  10418  fzss2  10419  fzp1elp1  10431  elfz1b  10446  elfz0fzfz0  10482  fz0fzelfz0  10483  difelfznle  10491  elfzofz  10519  nn0p1elfzo  10543  fzosplitsnm1  10576  ubmelm1fzo  10593  fzofzp1b  10595  fzosplitsn  10600  zsupcllemstep  10611  zsupcl  10613  infssfzcldc  10618  infssfzledc  10619  exbtwnz  10634  flqge0nn0  10677  flqge1nn  10678  zmodcl  10730  modqmuladdnn0  10754  modsumfzodifsn  10782  frec2uzf1od  10792  frec2uzisod  10793  frecuzrdgrrn  10794  frec2uzrdg  10795  frecuzrdgrcl  10796  frecuzrdgtcl  10798  frecuzrdgsuc  10800  frecuzrdgrclt  10801  frecuzrdgfunlem  10805  frecuzrdgtclt  10807  frecuzrdgsuctlem  10809  uzennn  10822  seq3fveq2  10861  seqfveq2g  10863  monoord  10871  iseqf1olemqcl  10885  iseqf1olemnab  10887  iseqf1olemab  10888  iseqf1olemqf1o  10892  seq3f1olemqsumkj  10897  seq3f1olemqsumk  10898  seq3id2  10912  exp3val  10927  expcl2lemap  10937  expclzaplem  10949  expge0  10961  expge1  10962  zsqcl2  11003  bcval4  11139  bcn1  11145  bccl2  11155  hashennnuni  11167  hashunlem  11193  hashdifpr  11210  zfz1isolem1  11237  seq3coll  11239  iswrdiz  11256  ccatsymb  11315  ccatrn  11322  ccat2s1fvwd  11360  swrds1  11385  swrdccat2  11388  swrdccatin2  11446  pfxccatin12lem2  11448  pfxccatin12lem3  11449  pfxccatin12  11450  pfxccat3  11451  pfxccat3a  11455  shftfn  11534  shftf  11540  recvguniq  11705  resqrexlemdecn  11722  rersqreu  11738  nn0abscl  11795  nnabscl  11810  abs2dif  11816  nn0maxcl  11935  climuni  12003  2clim  12011  climcn2  12019  summodclem2a  12092  fsum3  12098  fsum3cvg3  12107  fsumcl2lem  12109  fsumadd  12117  fisum0diag2  12158  fsummulc2  12159  fsumge0  12170  geolim2  12223  cvgratnnlemabsle  12238  cvgratz  12243  mertenslemi1  12246  prodmodclem3  12286  prodmodclem2a  12287  fprodeq0  12328  fprodge0  12348  eff2  12391  tanvalap  12419  zdvdsdc  12523  fzo0dvdseq  12568  oexpneg  12588  oddge22np1  12592  evennn02n  12593  evennn2n  12594  nno  12617  divalglemeunn  12632  divalglemex  12633  divalglemeuneg  12634  divalg  12635  bitsfzolem  12665  bitsinv1lem  12672  divgcdz  12692  bezoutlemmain  12719  bezoutlemmo  12727  bezoutlemeu  12728  bezoutlemle  12729  sqgcd  12750  uzwodc  12758  nninfctlemfo  12761  eucalgval2  12775  eucalglt  12779  lcmneg  12796  lcmgcdlem  12799  ncoprmgcdne1b  12811  prmind2  12842  prmdc  12852  sqnprm  12858  isprm5lem  12863  isprm5  12864  isprm6  12869  sqrt2irrlem  12883  pw2dvdseu  12890  sqpweven  12897  2sqpwodd  12898  sqrt2irrap  12902  qgt0numnn  12921  phicl2  12936  crth  12946  phimullem  12947  eulerthlem1  12949  eulerthlemh  12953  eulerthlemth  12954  hashgcdlem  12960  oddprm  12982  pythagtriplem6  12993  pythagtriplem11  12997  pythagtriplem13  12999  pythagtriplem19  13005  pclem0  13009  pcpremul  13016  pceu  13018  pc2dvds  13053  difsqpwdvds  13061  pcadd  13063  pockthlem  13079  pockthg  13080  1arith  13090  4sqlemffi  13119  4sqlem11  13124  4sqlem12  13125  4sqlem13m  13126  4sqlem14  13127  4sqlem17  13130  ballotfilemic  13194  ballotfilem1c  13195  ballotfilemrc  13218  ballotfilemth  13225  oddennn  13227  evenennn  13228  ennnfoneleminc  13246  ennnfonelemf1  13253  ennnfonelemen  13256  exmidunben  13261  ctinf  13265  ctiunctlemfo  13274  nninfdclemlt  13286  nninfdclemf1  13287  ptex  13561  imasaddfnlemg  13578  imasaddflemg  13580  mgmsscl  13624  sgrp0  13673  sgrp1  13674  hashfinmndnn  13693  ismndd  13698  mndpfo  13699  mhmf1o  13725  0mhm  13741  resmhm  13742  resmhm2  13743  resmhm2b  13744  mhmco  13745  gsumvallem2  13748  isgrpd2e  13775  grpinvf1o  13825  grpinvnzcl  13827  dfgrp3m  13854  mhmmnd  13869  ghmgrp  13871  mulgval  13875  mulgfng  13877  subgmulg  13941  issubg4m  13946  isnsg3  13960  nmzsubg  13963  ssnmz  13964  0nsg  13967  nsgid  13968  ghmnsgima  14021  ghmnsgpreima  14022  ghmf1  14026  kerf1ghm  14027  ghmf1o  14028  conjnmzb  14033  isabld  14052  ghmcmn  14080  ghmabl  14081  invghm  14082  gfsumval  14102  srgfcl  14216  srglmhm  14236  srgrmhm  14237  iscrngd  14285  ringsrg  14290  unitabl  14362  rhmf1o  14413  rhmco  14419  ringelnzr  14432  subrngringnsg  14451  subrgcrng  14471  subrgnzr  14488  resrhm  14494  unitrrg  14514  aprnzr  14537  aprlring  14538  drngnzr  14557  lssneln0  14648  rnglidlmsgrp  14771  quscrng  14807  expghmap  14881  mulgghm2  14882  znf1o  14925  znidom  14931  znidomb  14932  psrbaglesuppg  14947  psrbagcon  14952  tgtopon  15057  distopon  15078  epttop  15081  resttopon  15162  resttopon2  15169  cnco  15212  lmss  15237  txtopon  15253  uptx  15265  txdis1cn  15269  hmeocnv  15298  hmeof1o2  15299  hmeores  15306  hmeoco  15307  idhmeo  15308  txhmeo  15310  txswaphmeo  15312  psmetxrge0  15323  isxmet2d  15339  metres2  15372  xmetresbl  15431  comet  15490  bdxmet  15492  bdmet  15493  tgioo  15545  mulc1cncf  15580  mulcncflem  15598  cnrehmeocntop  15601  cnopnap  15602  dedekindeu  15614  dedekindicclemicc  15623  ivthinclemlm  15625  ivthinclemum  15626  ivthinclemlopn  15627  ivthinclemlr  15628  ivthinclemuopn  15629  ivthinclemur  15630  ivthinclemloc  15632  ivthinc  15634  ivthreinc  15636  dvfgg  15679  dvcjbr  15699  dvcj  15700  dvfre  15701  elplyr  15731  plyreres  15755  rplogbval  15936  sgmnncl  15982  mpodvdsmulf1o  15984  mersenne  15991  perfectlem2  15994  lgsfcl2  16005  lgsval2lem  16009  lgsmod  16025  lgsdirprm  16033  lgsne0  16037  gausslemma2dlem0h  16055  gausslemma2dlem1a  16057  gausslemma2dlem1f1o  16059  gausslemma2dlem4  16063  lgseisenlem1  16069  lgseisenlem2  16070  lgsquadlem1  16076  lgsquadlem2  16077  lgsquad2lem2  16081  2sqlem8  16122  2sqlem9  16123  structiedg0val  16161  ausgrumgrien  16291  usgredgreu  16337  uspgredg2vtxeu  16339  uspgredg2v  16342  usgredg2v  16345  usgr1e  16362  subuhgr  16393  subupgr  16394  subumgr  16395  subusgr  16396  vdegp1aid  16435  trlres  16511  clwwlkbp  16516  clwwlkccatlem  16521  s2elclwwlknon2  16557  clwwlknonex2lem2  16559  clwwlknonex2e  16561  bj-charfundcALT  16705  bj-nnord  16854  bj-inf2vnlem1  16866  pwf1oexmid  16899  nnsf  16909  nninfall  16913  nninfself  16917  exmidsbthrlem  16928  qdencn  16933