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  940  ecase2d  1387  sb2  1815  sbequ1  1816  sbidm  1899  eqeu  2976  euind  2993  reuind  3011  eldifd  3210  eqssd  3244  ssrabdv  3306  elind  3392  dcun  3604  opm  4326  issod  4416  ordsucim  4598  onintonm  4615  ordtri2or2exmidlem  4624  en2lp  4652  ordwe  4674  sosng  4799  sotri2  5134  sotri3  5135  relssdmrn  5257  funun  5371  fnsng  5377  fnprg  5385  fntpg  5386  fntp  5387  fununi  5398  imain  5412  fnco  5440  f00  5528  f1ss  5548  f1ssr  5549  f1ssres  5551  f1f1orn  5594  foimacnv  5601  foun  5602  fun11iun  5604  sefvex  5660  dff3im  5792  fmpt  5797  ffnfv  5805  fmpt2d  5809  ffvresb  5810  fprg  5837  foco2  5894  fcof1  5924  fcofo  5925  fcof1o  5930  fliftf  5940  isoini2  5960  f1oiso  5967  moriotass  6002  fnoprabg  6122  f1ocnvd  6225  suppssfv  6231  suppssov1  6232  1stcof  6326  2ndcof  6327  1stconst  6386  2ndconst  6387  fo2ndf  6392  f1o2ndf1  6393  f1od2  6400  smores2  6460  tfrlem5  6480  tfrlemibfn  6494  tfr1onlembfn  6510  tfri1dALT  6517  tfrcllembfn  6523  nntri2  6662  eroveu  6795  elixpsn  6904  dom2lem  6945  xpf1o  7030  fidifsnen  7057  finexdc  7092  elssdc  7094  unfidisj  7114  f1finf1o  7146  fidcenumlemrks  7152  sbthlemi9  7164  supeuti  7193  infeuti  7228  casef1  7289  caseinl  7290  caseinr  7291  difinfsnlem  7298  ctmlemr  7307  ctm  7308  ctssdclemn0  7309  ctssdccl  7310  ctssdc  7312  enumctlemm  7313  nnnninf  7325  nninfwlpoimlemg  7374  en2other2  7407  exmidfodomrlemim  7412  pw1if  7443  pw1nel3  7449  dftap2  7470  cc2lem  7485  cc4f  7488  addclpi  7547  mulclpi  7548  nnppipi  7563  recmulnqg  7611  enq0ref  7653  nqnq0pi  7658  genipv  7729  addclpr  7757  nqprxx  7766  prmuloc  7786  mulclpr  7792  distrlem1prl  7802  distrlem1pru  7803  ltexprlempr  7828  ltexprlemrl  7830  ltexprlemru  7832  lteupri  7837  recexprlempr  7852  cauappcvgprlemm  7865  cauappcvgprlemopl  7866  cauappcvgprlemlol  7867  cauappcvgprlemopu  7868  cauappcvgprlemupu  7869  cauappcvgprlemloc  7872  cauappcvgprlemcl  7873  cauappcvgprlemladdfu  7874  cauappcvgprlemladdfl  7875  cauappcvgprlem2  7880  caucvgprlemm  7888  caucvgprlemopl  7889  caucvgprlemlol  7890  caucvgprlemopu  7891  caucvgprlemupu  7892  caucvgprlemloc  7895  caucvgprlemcl  7896  caucvgprlemladdfu  7897  caucvgprlem2  7900  caucvgprprlemml  7914  caucvgprprlemmu  7915  caucvgprprlemopl  7917  caucvgprprlemlol  7918  caucvgprprlemopu  7919  caucvgprprlemupu  7920  caucvgprprlemloc  7923  caucvgprprlemcl  7924  caucvgprprlem2  7930  suplocexprlemex  7942  suplocsrlem  8028  elrealeu  8049  rereceu  8109  axpre-suploclemres  8121  negf1o  8561  aptap  8830  receuap  8849  divvalap  8854  cju  9141  nn0ge2m1nn  9462  nnnegz  9482  elnnz  9489  elnn0z  9492  peano2z  9515  nn0n0n1ge2  9550  msqznn  9580  eluzaddi  9783  eluzsubi  9784  uzind4  9822  supinfneg  9829  infsupneg  9830  elnn1uz2  9841  uz2mulcl  9842  divfnzn  9855  nnrp  9898  rpaddcl  9912  rpmulcl  9913  rpdivcl  9914  rpgecl  9917  ge0p1rp  9920  elrpd  9928  ge0addcl  10216  ge0mulcl  10217  ge0xaddcl  10218  icoshftf1o  10226  peano2fzr  10272  uzsubsubfz  10282  fzsplit2  10285  elfznn  10289  fzss1  10298  fzss2  10299  fzp1elp1  10310  elfz1b  10325  elfz0fzfz0  10361  fz0fzelfz0  10362  difelfznle  10370  elfzofz  10398  nn0p1elfzo  10422  fzosplitsnm1  10455  ubmelm1fzo  10472  fzofzp1b  10474  fzosplitsn  10479  zsupcllemstep  10490  zsupcl  10492  exbtwnz  10511  flqge0nn0  10554  flqge1nn  10555  zmodcl  10607  modqmuladdnn0  10631  modsumfzodifsn  10659  frec2uzf1od  10669  frec2uzisod  10670  frecuzrdgrrn  10671  frec2uzrdg  10672  frecuzrdgrcl  10673  frecuzrdgtcl  10675  frecuzrdgsuc  10677  frecuzrdgrclt  10678  frecuzrdgfunlem  10682  frecuzrdgtclt  10684  frecuzrdgsuctlem  10686  uzennn  10699  seq3fveq2  10738  seqfveq2g  10740  monoord  10748  iseqf1olemqcl  10762  iseqf1olemnab  10764  iseqf1olemab  10765  iseqf1olemqf1o  10769  seq3f1olemqsumkj  10774  seq3f1olemqsumk  10775  seq3id2  10789  exp3val  10804  expcl2lemap  10814  expclzaplem  10826  expge0  10838  expge1  10839  zsqcl2  10880  bcval4  11015  bcn1  11021  bccl2  11031  hashennnuni  11042  hashunlem  11068  hashdifpr  11085  zfz1isolem1  11105  seq3coll  11107  iswrdiz  11124  ccatsymb  11183  ccatrn  11190  ccat2s1fvwd  11228  swrds1  11253  swrdccat2  11256  swrdccatin2  11314  pfxccatin12lem2  11316  pfxccatin12lem3  11317  pfxccatin12  11318  pfxccat3  11319  pfxccat3a  11323  shftfn  11402  shftf  11408  recvguniq  11573  resqrexlemdecn  11590  rersqreu  11606  nn0abscl  11663  nnabscl  11678  abs2dif  11684  nn0maxcl  11803  climuni  11871  2clim  11879  climcn2  11887  summodclem2a  11960  fsum3  11966  fsum3cvg3  11975  fsumcl2lem  11977  fsumadd  11985  fisum0diag2  12026  fsummulc2  12027  fsumge0  12038  geolim2  12091  cvgratnnlemabsle  12106  cvgratz  12111  mertenslemi1  12114  prodmodclem3  12154  prodmodclem2a  12155  fprodeq0  12196  fprodge0  12216  eff2  12259  tanvalap  12287  zdvdsdc  12391  fzo0dvdseq  12436  oexpneg  12456  oddge22np1  12460  evennn02n  12461  evennn2n  12462  nno  12485  divalglemeunn  12500  divalglemex  12501  divalglemeuneg  12502  divalg  12503  bitsfzolem  12533  bitsinv1lem  12540  divgcdz  12560  bezoutlemmain  12587  bezoutlemmo  12595  bezoutlemeu  12596  bezoutlemle  12597  sqgcd  12618  uzwodc  12626  nninfctlemfo  12629  eucalgval2  12643  eucalglt  12647  lcmneg  12664  lcmgcdlem  12667  ncoprmgcdne1b  12679  prmind2  12710  prmdc  12720  sqnprm  12726  isprm5lem  12731  isprm5  12732  isprm6  12737  sqrt2irrlem  12751  pw2dvdseu  12758  sqpweven  12765  2sqpwodd  12766  sqrt2irrap  12770  qgt0numnn  12789  phicl2  12804  hashdvds  12811  crth  12814  phimullem  12815  eulerthlem1  12817  eulerthlemh  12821  eulerthlemth  12822  hashgcdlem  12828  oddprm  12850  pythagtriplem6  12861  pythagtriplem11  12865  pythagtriplem13  12867  pythagtriplem19  12873  pclem0  12877  pcpremul  12884  pceu  12886  pc2dvds  12921  difsqpwdvds  12929  pcadd  12931  pockthlem  12947  pockthg  12948  1arith  12958  4sqlemffi  12987  4sqlem11  12992  4sqlem12  12993  4sqlem13m  12994  4sqlem14  12995  4sqlem17  12998  oddennn  13031  evenennn  13032  ennnfoneleminc  13050  ennnfonelemf1  13057  ennnfonelemen  13060  exmidunben  13065  ctinf  13069  ctiunctlemfo  13078  nninfdclemlt  13090  nninfdclemf1  13091  ptex  13365  imasaddfnlemg  13415  imasaddflemg  13417  mgmsscl  13462  sgrp0  13511  sgrp1  13512  hashfinmndnn  13533  ismndd  13538  mndpfo  13539  mhmf1o  13571  0mhm  13587  resmhm  13588  resmhm2  13589  resmhm2b  13590  mhmco  13591  gsumvallem2  13594  isgrpd2e  13621  grpinvf1o  13671  grpinvnzcl  13673  dfgrp3m  13700  mhmmnd  13721  ghmgrp  13723  mulgval  13727  mulgfng  13729  subgmulg  13793  issubg4m  13798  isnsg3  13812  nmzsubg  13815  ssnmz  13816  0nsg  13819  nsgid  13820  ghmnsgima  13873  ghmnsgpreima  13874  ghmf1  13878  kerf1ghm  13879  ghmf1o  13880  conjnmzb  13885  isabld  13904  ghmcmn  13932  ghmabl  13933  invghm  13934  srgfcl  14005  srglmhm  14025  srgrmhm  14026  iscrngd  14074  ringsrg  14079  unitabl  14150  rhmf1o  14201  rhmco  14207  ringelnzr  14220  subrngringnsg  14238  subrgcrng  14258  subrgnzr  14275  resrhm  14281  unitrrg  14300  lssneln0  14407  rnglidlmsgrp  14530  quscrng  14566  expghmap  14640  mulgghm2  14641  znf1o  14684  znidom  14690  znidomb  14691  psrbaglesuppg  14705  tgtopon  14809  distopon  14830  epttop  14833  resttopon  14914  resttopon2  14921  cnco  14964  lmss  14989  txtopon  15005  uptx  15017  txdis1cn  15021  hmeocnv  15050  hmeof1o2  15051  hmeores  15058  hmeoco  15059  idhmeo  15060  txhmeo  15062  txswaphmeo  15064  psmetxrge0  15075  isxmet2d  15091  metres2  15124  xmetresbl  15183  comet  15242  bdxmet  15244  bdmet  15245  tgioo  15297  mulc1cncf  15332  mulcncflem  15350  cnrehmeocntop  15353  cnopnap  15354  dedekindeu  15366  dedekindicclemicc  15375  ivthinclemlm  15377  ivthinclemum  15378  ivthinclemlopn  15379  ivthinclemlr  15380  ivthinclemuopn  15381  ivthinclemur  15382  ivthinclemloc  15384  ivthinc  15386  ivthreinc  15388  dvfgg  15431  dvcjbr  15451  dvcj  15452  dvfre  15453  elplyr  15483  plyreres  15507  rplogbval  15688  sgmnncl  15731  mpodvdsmulf1o  15733  mersenne  15740  perfectlem2  15743  lgsfcl2  15754  lgsval2lem  15758  lgsmod  15774  lgsdirprm  15782  lgsne0  15786  gausslemma2dlem0h  15804  gausslemma2dlem1a  15806  gausslemma2dlem1f1o  15808  gausslemma2dlem4  15812  lgseisenlem1  15818  lgseisenlem2  15819  lgsquadlem1  15825  lgsquadlem2  15826  lgsquad2lem2  15830  2sqlem8  15871  2sqlem9  15872  structiedg0val  15910  ausgrumgrien  16040  usgredgreu  16086  uspgredg2vtxeu  16088  uspgredg2v  16091  usgredg2v  16094  usgr1e  16111  subuhgr  16142  subupgr  16143  subumgr  16144  subusgr  16145  vdegp1aid  16184  trlres  16260  clwwlkbp  16265  clwwlkccatlem  16270  s2elclwwlknon2  16306  clwwlknonex2lem2  16308  clwwlknonex2e  16310  bj-charfundcALT  16455  bj-nnord  16604  bj-inf2vnlem1  16616  pwf1oexmid  16651  nnsf  16658  nninfall  16662  nninfself  16666  exmidsbthrlem  16677  qdencn  16682  gfsumval  16732