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  938  ecase2d  1385  sb2  1813  sbequ1  1814  sbidm  1897  eqeu  2973  euind  2990  reuind  3008  eldifd  3207  eqssd  3241  ssrabdv  3303  elind  3389  dcun  3601  opm  4319  issod  4409  ordsucim  4591  onintonm  4608  ordtri2or2exmidlem  4617  en2lp  4645  ordwe  4667  sosng  4791  sotri2  5125  sotri3  5126  relssdmrn  5248  funun  5361  fnsng  5367  fnprg  5375  fntpg  5376  fntp  5377  fununi  5388  imain  5402  fnco  5430  f00  5516  f1ss  5536  f1ssr  5537  f1ssres  5539  f1f1orn  5582  foimacnv  5589  foun  5590  fun11iun  5592  sefvex  5647  dff3im  5779  fmpt  5784  ffnfv  5792  fmpt2d  5796  ffvresb  5797  fprg  5821  foco2  5876  fcof1  5906  fcofo  5907  fcof1o  5912  fliftf  5922  isoini2  5942  f1oiso  5949  moriotass  5984  fnoprabg  6104  f1ocnvd  6206  suppssfv  6212  suppssov1  6213  1stcof  6307  2ndcof  6308  1stconst  6365  2ndconst  6366  fo2ndf  6371  f1o2ndf1  6372  f1od2  6379  smores2  6438  tfrlem5  6458  tfrlemibfn  6472  tfr1onlembfn  6488  tfri1dALT  6495  tfrcllembfn  6501  nntri2  6638  eroveu  6771  elixpsn  6880  dom2lem  6921  xpf1o  7001  fidifsnen  7028  finexdc  7060  unfidisj  7080  f1finf1o  7110  fidcenumlemrks  7116  sbthlemi9  7128  supeuti  7157  infeuti  7192  casef1  7253  caseinl  7254  caseinr  7255  difinfsnlem  7262  ctmlemr  7271  ctm  7272  ctssdclemn0  7273  ctssdccl  7274  ctssdc  7276  enumctlemm  7277  nnnninf  7289  nninfwlpoimlemg  7338  en2other2  7370  exmidfodomrlemim  7375  pw1if  7406  pw1nel3  7412  dftap2  7433  cc2lem  7448  cc4f  7451  addclpi  7510  mulclpi  7511  nnppipi  7526  recmulnqg  7574  enq0ref  7616  nqnq0pi  7621  genipv  7692  addclpr  7720  nqprxx  7729  prmuloc  7749  mulclpr  7755  distrlem1prl  7765  distrlem1pru  7766  ltexprlempr  7791  ltexprlemrl  7793  ltexprlemru  7795  lteupri  7800  recexprlempr  7815  cauappcvgprlemm  7828  cauappcvgprlemopl  7829  cauappcvgprlemlol  7830  cauappcvgprlemopu  7831  cauappcvgprlemupu  7832  cauappcvgprlemloc  7835  cauappcvgprlemcl  7836  cauappcvgprlemladdfu  7837  cauappcvgprlemladdfl  7838  cauappcvgprlem2  7843  caucvgprlemm  7851  caucvgprlemopl  7852  caucvgprlemlol  7853  caucvgprlemopu  7854  caucvgprlemupu  7855  caucvgprlemloc  7858  caucvgprlemcl  7859  caucvgprlemladdfu  7860  caucvgprlem2  7863  caucvgprprlemml  7877  caucvgprprlemmu  7878  caucvgprprlemopl  7880  caucvgprprlemlol  7881  caucvgprprlemopu  7882  caucvgprprlemupu  7883  caucvgprprlemloc  7886  caucvgprprlemcl  7887  caucvgprprlem2  7893  suplocexprlemex  7905  suplocsrlem  7991  elrealeu  8012  rereceu  8072  axpre-suploclemres  8084  negf1o  8524  aptap  8793  receuap  8812  divvalap  8817  cju  9104  nn0ge2m1nn  9425  nnnegz  9445  elnnz  9452  elnn0z  9455  peano2z  9478  nn0n0n1ge2  9513  msqznn  9543  eluzaddi  9745  eluzsubi  9746  uzind4  9779  supinfneg  9786  infsupneg  9787  elnn1uz2  9798  uz2mulcl  9799  divfnzn  9812  nnrp  9855  rpaddcl  9869  rpmulcl  9870  rpdivcl  9871  rpgecl  9874  ge0p1rp  9877  elrpd  9885  ge0addcl  10173  ge0mulcl  10174  ge0xaddcl  10175  icoshftf1o  10183  peano2fzr  10229  uzsubsubfz  10239  fzsplit2  10242  elfznn  10246  fzss1  10255  fzss2  10256  fzp1elp1  10267  elfz1b  10282  elfz0fzfz0  10318  fz0fzelfz0  10319  difelfznle  10327  elfzofz  10355  fzosplitsnm1  10410  ubmelm1fzo  10427  fzofzp1b  10429  fzosplitsn  10434  zsupcllemstep  10444  zsupcl  10446  exbtwnz  10465  flqge0nn0  10508  flqge1nn  10509  zmodcl  10561  modqmuladdnn0  10585  modsumfzodifsn  10613  frec2uzf1od  10623  frec2uzisod  10624  frecuzrdgrrn  10625  frec2uzrdg  10626  frecuzrdgrcl  10627  frecuzrdgtcl  10629  frecuzrdgsuc  10631  frecuzrdgrclt  10632  frecuzrdgfunlem  10636  frecuzrdgtclt  10638  frecuzrdgsuctlem  10640  uzennn  10653  seq3fveq2  10692  seqfveq2g  10694  monoord  10702  iseqf1olemqcl  10716  iseqf1olemnab  10718  iseqf1olemab  10719  iseqf1olemqf1o  10723  seq3f1olemqsumkj  10728  seq3f1olemqsumk  10729  seq3id2  10743  exp3val  10758  expcl2lemap  10768  expclzaplem  10780  expge0  10792  expge1  10793  zsqcl2  10834  bcval4  10969  bcn1  10975  bccl2  10985  hashennnuni  10996  hashunlem  11021  hashdifpr  11037  zfz1isolem1  11057  seq3coll  11059  iswrdiz  11073  ccatsymb  11132  ccatrn  11139  swrds1  11195  swrdccat2  11198  swrdccatin2  11256  pfxccatin12lem2  11258  pfxccatin12lem3  11259  pfxccatin12  11260  pfxccat3  11261  pfxccat3a  11265  shftfn  11330  shftf  11336  recvguniq  11501  resqrexlemdecn  11518  rersqreu  11534  nn0abscl  11591  nnabscl  11606  abs2dif  11612  nn0maxcl  11731  climuni  11799  2clim  11807  climcn2  11815  summodclem2a  11887  fsum3  11893  fsum3cvg3  11902  fsumcl2lem  11904  fsumadd  11912  fisum0diag2  11953  fsummulc2  11954  fsumge0  11965  geolim2  12018  cvgratnnlemabsle  12033  cvgratz  12038  mertenslemi1  12041  prodmodclem3  12081  prodmodclem2a  12082  fprodeq0  12123  fprodge0  12143  eff2  12186  tanvalap  12214  zdvdsdc  12318  fzo0dvdseq  12363  oexpneg  12383  oddge22np1  12387  evennn02n  12388  evennn2n  12389  nno  12412  divalglemeunn  12427  divalglemex  12428  divalglemeuneg  12429  divalg  12430  bitsfzolem  12460  bitsinv1lem  12467  divgcdz  12487  bezoutlemmain  12514  bezoutlemmo  12522  bezoutlemeu  12523  bezoutlemle  12524  sqgcd  12545  uzwodc  12553  nninfctlemfo  12556  eucalgval2  12570  eucalglt  12574  lcmneg  12591  lcmgcdlem  12594  ncoprmgcdne1b  12606  prmind2  12637  prmdc  12647  sqnprm  12653  isprm5lem  12658  isprm5  12659  isprm6  12664  sqrt2irrlem  12678  pw2dvdseu  12685  sqpweven  12692  2sqpwodd  12693  sqrt2irrap  12697  qgt0numnn  12716  phicl2  12731  hashdvds  12738  crth  12741  phimullem  12742  eulerthlem1  12744  eulerthlemh  12748  eulerthlemth  12749  hashgcdlem  12755  oddprm  12777  pythagtriplem6  12788  pythagtriplem11  12792  pythagtriplem13  12794  pythagtriplem19  12800  pclem0  12804  pcpremul  12811  pceu  12813  pc2dvds  12848  difsqpwdvds  12856  pcadd  12858  pockthlem  12874  pockthg  12875  1arith  12885  4sqlemffi  12914  4sqlem11  12919  4sqlem12  12920  4sqlem13m  12921  4sqlem14  12922  4sqlem17  12925  oddennn  12958  evenennn  12959  ennnfoneleminc  12977  ennnfonelemf1  12984  ennnfonelemen  12987  exmidunben  12992  ctinf  12996  ctiunctlemfo  13005  nninfdclemlt  13017  nninfdclemf1  13018  ptex  13292  imasaddfnlemg  13342  imasaddflemg  13344  mgmsscl  13389  sgrp0  13438  sgrp1  13439  hashfinmndnn  13460  ismndd  13465  mndpfo  13466  mhmf1o  13498  0mhm  13514  resmhm  13515  resmhm2  13516  resmhm2b  13517  mhmco  13518  gsumvallem2  13521  isgrpd2e  13548  grpinvf1o  13598  grpinvnzcl  13600  dfgrp3m  13627  mhmmnd  13648  ghmgrp  13650  mulgval  13654  mulgfng  13656  subgmulg  13720  issubg4m  13725  isnsg3  13739  nmzsubg  13742  ssnmz  13743  0nsg  13746  nsgid  13747  ghmnsgima  13800  ghmnsgpreima  13801  ghmf1  13805  kerf1ghm  13806  ghmf1o  13807  conjnmzb  13812  isabld  13831  ghmcmn  13859  ghmabl  13860  invghm  13861  srgfcl  13931  srglmhm  13951  srgrmhm  13952  iscrngd  14000  ringsrg  14005  unitabl  14075  rhmf1o  14126  rhmco  14132  ringelnzr  14145  subrngringnsg  14163  subrgcrng  14183  subrgnzr  14200  resrhm  14206  unitrrg  14225  lssneln0  14332  rnglidlmsgrp  14455  quscrng  14491  expghmap  14565  mulgghm2  14566  znf1o  14609  znidom  14615  znidomb  14616  psrbaglesuppg  14630  tgtopon  14734  distopon  14755  epttop  14758  resttopon  14839  resttopon2  14846  cnco  14889  lmss  14914  txtopon  14930  uptx  14942  txdis1cn  14946  hmeocnv  14975  hmeof1o2  14976  hmeores  14983  hmeoco  14984  idhmeo  14985  txhmeo  14987  txswaphmeo  14989  psmetxrge0  15000  isxmet2d  15016  metres2  15049  xmetresbl  15108  comet  15167  bdxmet  15169  bdmet  15170  tgioo  15222  mulc1cncf  15257  mulcncflem  15275  cnrehmeocntop  15278  cnopnap  15279  dedekindeu  15291  dedekindicclemicc  15300  ivthinclemlm  15302  ivthinclemum  15303  ivthinclemlopn  15304  ivthinclemlr  15305  ivthinclemuopn  15306  ivthinclemur  15307  ivthinclemloc  15309  ivthinc  15311  ivthreinc  15313  dvfgg  15356  dvcjbr  15376  dvcj  15377  dvfre  15378  elplyr  15408  plyreres  15432  rplogbval  15613  sgmnncl  15656  mpodvdsmulf1o  15658  mersenne  15665  perfectlem2  15668  lgsfcl2  15679  lgsval2lem  15683  lgsmod  15699  lgsdirprm  15707  lgsne0  15711  gausslemma2dlem0h  15729  gausslemma2dlem1a  15731  gausslemma2dlem1f1o  15733  gausslemma2dlem4  15737  lgseisenlem1  15743  lgseisenlem2  15744  lgsquadlem1  15750  lgsquadlem2  15751  lgsquad2lem2  15755  2sqlem8  15796  2sqlem9  15797  structiedg0val  15835  ausgrumgrien  15962  usgredgreu  16008  uspgredg2vtxeu  16010  uspgredg2v  16013  usgredg2v  16016  bj-charfundcALT  16130  bj-nnord  16279  bj-inf2vnlem1  16291  pwf1oexmid  16324  nnsf  16330  nninfall  16334  nninfself  16338  exmidsbthrlem  16349  qdencn  16354