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  935  sb2  1791  sbequ1  1792  sbidm  1875  eqeu  2950  euind  2967  reuind  2985  eldifd  3184  eqssd  3218  ssrabdv  3280  elind  3366  dcun  3578  opm  4296  issod  4384  ordsucim  4566  onintonm  4583  ordtri2or2exmidlem  4592  en2lp  4620  ordwe  4642  sosng  4766  sotri2  5099  sotri3  5100  relssdmrn  5222  funun  5334  fnsng  5340  fnprg  5348  fntpg  5349  fntp  5350  fununi  5361  imain  5375  fnco  5403  f00  5489  f1ss  5509  f1ssr  5510  f1ssres  5512  f1f1orn  5555  foimacnv  5562  foun  5563  fun11iun  5565  sefvex  5620  dff3im  5748  fmpt  5753  ffnfv  5761  fmpt2d  5765  ffvresb  5766  fprg  5790  foco2  5845  fcof1  5875  fcofo  5876  fcof1o  5881  fliftf  5891  isoini2  5911  f1oiso  5918  moriotass  5951  fnoprabg  6069  f1ocnvd  6171  suppssfv  6177  suppssov1  6178  1stcof  6272  2ndcof  6273  1stconst  6330  2ndconst  6331  fo2ndf  6336  f1o2ndf1  6337  f1od2  6344  smores2  6403  tfrlem5  6423  tfrlemibfn  6437  tfr1onlembfn  6453  tfri1dALT  6460  tfrcllembfn  6466  nntri2  6603  eroveu  6736  elixpsn  6845  dom2lem  6886  xpf1o  6966  fidifsnen  6993  finexdc  7025  unfidisj  7045  f1finf1o  7075  fidcenumlemrks  7081  sbthlemi9  7093  supeuti  7122  infeuti  7157  casef1  7218  caseinl  7219  caseinr  7220  difinfsnlem  7227  ctmlemr  7236  ctm  7237  ctssdclemn0  7238  ctssdccl  7239  ctssdc  7241  enumctlemm  7242  nnnninf  7254  nninfwlpoimlemg  7303  en2other2  7335  exmidfodomrlemim  7340  pw1if  7371  pw1nel3  7377  dftap2  7398  cc2lem  7413  cc4f  7416  addclpi  7475  mulclpi  7476  nnppipi  7491  recmulnqg  7539  enq0ref  7581  nqnq0pi  7586  genipv  7657  addclpr  7685  nqprxx  7694  prmuloc  7714  mulclpr  7720  distrlem1prl  7730  distrlem1pru  7731  ltexprlempr  7756  ltexprlemrl  7758  ltexprlemru  7760  lteupri  7765  recexprlempr  7780  cauappcvgprlemm  7793  cauappcvgprlemopl  7794  cauappcvgprlemlol  7795  cauappcvgprlemopu  7796  cauappcvgprlemupu  7797  cauappcvgprlemloc  7800  cauappcvgprlemcl  7801  cauappcvgprlemladdfu  7802  cauappcvgprlemladdfl  7803  cauappcvgprlem2  7808  caucvgprlemm  7816  caucvgprlemopl  7817  caucvgprlemlol  7818  caucvgprlemopu  7819  caucvgprlemupu  7820  caucvgprlemloc  7823  caucvgprlemcl  7824  caucvgprlemladdfu  7825  caucvgprlem2  7828  caucvgprprlemml  7842  caucvgprprlemmu  7843  caucvgprprlemopl  7845  caucvgprprlemlol  7846  caucvgprprlemopu  7847  caucvgprprlemupu  7848  caucvgprprlemloc  7851  caucvgprprlemcl  7852  caucvgprprlem2  7858  suplocexprlemex  7870  suplocsrlem  7956  elrealeu  7977  rereceu  8037  axpre-suploclemres  8049  negf1o  8489  aptap  8758  receuap  8777  divvalap  8782  cju  9069  nn0ge2m1nn  9390  nnnegz  9410  elnnz  9417  elnn0z  9420  peano2z  9443  nn0n0n1ge2  9478  msqznn  9508  eluzaddi  9710  eluzsubi  9711  uzind4  9744  supinfneg  9751  infsupneg  9752  elnn1uz2  9763  uz2mulcl  9764  divfnzn  9777  nnrp  9820  rpaddcl  9834  rpmulcl  9835  rpdivcl  9836  rpgecl  9839  ge0p1rp  9842  elrpd  9850  ge0addcl  10138  ge0mulcl  10139  ge0xaddcl  10140  icoshftf1o  10148  peano2fzr  10194  uzsubsubfz  10204  fzsplit2  10207  elfznn  10211  fzss1  10220  fzss2  10221  fzp1elp1  10232  elfz1b  10247  elfz0fzfz0  10283  fz0fzelfz0  10284  difelfznle  10292  elfzofz  10320  fzosplitsnm1  10375  ubmelm1fzo  10392  fzofzp1b  10394  fzosplitsn  10399  zsupcllemstep  10409  zsupcl  10411  exbtwnz  10430  flqge0nn0  10473  flqge1nn  10474  zmodcl  10526  modqmuladdnn0  10550  modsumfzodifsn  10578  frec2uzf1od  10588  frec2uzisod  10589  frecuzrdgrrn  10590  frec2uzrdg  10591  frecuzrdgrcl  10592  frecuzrdgtcl  10594  frecuzrdgsuc  10596  frecuzrdgrclt  10597  frecuzrdgfunlem  10601  frecuzrdgtclt  10603  frecuzrdgsuctlem  10605  uzennn  10618  seq3fveq2  10657  seqfveq2g  10659  monoord  10667  iseqf1olemqcl  10681  iseqf1olemnab  10683  iseqf1olemab  10684  iseqf1olemqf1o  10688  seq3f1olemqsumkj  10693  seq3f1olemqsumk  10694  seq3id2  10708  exp3val  10723  expcl2lemap  10733  expclzaplem  10745  expge0  10757  expge1  10758  zsqcl2  10799  bcval4  10934  bcn1  10940  bccl2  10950  hashennnuni  10961  hashunlem  10986  hashdifpr  11002  zfz1isolem1  11022  seq3coll  11024  iswrdiz  11038  ccatsymb  11096  ccatrn  11103  swrds1  11159  swrdccat2  11162  swrdccatin2  11220  pfxccatin12lem2  11222  pfxccatin12lem3  11223  pfxccatin12  11224  pfxccat3  11225  pfxccat3a  11229  shftfn  11250  shftf  11256  recvguniq  11421  resqrexlemdecn  11438  rersqreu  11454  nn0abscl  11511  nnabscl  11526  abs2dif  11532  nn0maxcl  11651  climuni  11719  2clim  11727  climcn2  11735  summodclem2a  11807  fsum3  11813  fsum3cvg3  11822  fsumcl2lem  11824  fsumadd  11832  fisum0diag2  11873  fsummulc2  11874  fsumge0  11885  geolim2  11938  cvgratnnlemabsle  11953  cvgratz  11958  mertenslemi1  11961  prodmodclem3  12001  prodmodclem2a  12002  fprodeq0  12043  fprodge0  12063  eff2  12106  tanvalap  12134  zdvdsdc  12238  fzo0dvdseq  12283  oexpneg  12303  oddge22np1  12307  evennn02n  12308  evennn2n  12309  nno  12332  divalglemeunn  12347  divalglemex  12348  divalglemeuneg  12349  divalg  12350  bitsfzolem  12380  bitsinv1lem  12387  divgcdz  12407  bezoutlemmain  12434  bezoutlemmo  12442  bezoutlemeu  12443  bezoutlemle  12444  sqgcd  12465  uzwodc  12473  nninfctlemfo  12476  eucalgval2  12490  eucalglt  12494  lcmneg  12511  lcmgcdlem  12514  ncoprmgcdne1b  12526  prmind2  12557  prmdc  12567  sqnprm  12573  isprm5lem  12578  isprm5  12579  isprm6  12584  sqrt2irrlem  12598  pw2dvdseu  12605  sqpweven  12612  2sqpwodd  12613  sqrt2irrap  12617  qgt0numnn  12636  phicl2  12651  hashdvds  12658  crth  12661  phimullem  12662  eulerthlem1  12664  eulerthlemh  12668  eulerthlemth  12669  hashgcdlem  12675  oddprm  12697  pythagtriplem6  12708  pythagtriplem11  12712  pythagtriplem13  12714  pythagtriplem19  12720  pclem0  12724  pcpremul  12731  pceu  12733  pc2dvds  12768  difsqpwdvds  12776  pcadd  12778  pockthlem  12794  pockthg  12795  1arith  12805  4sqlemffi  12834  4sqlem11  12839  4sqlem12  12840  4sqlem13m  12841  4sqlem14  12842  4sqlem17  12845  oddennn  12878  evenennn  12879  ennnfoneleminc  12897  ennnfonelemf1  12904  ennnfonelemen  12907  exmidunben  12912  ctinf  12916  ctiunctlemfo  12925  nninfdclemlt  12937  nninfdclemf1  12938  ptex  13211  imasaddfnlemg  13261  imasaddflemg  13263  mgmsscl  13308  sgrp0  13357  sgrp1  13358  hashfinmndnn  13379  ismndd  13384  mndpfo  13385  mhmf1o  13417  0mhm  13433  resmhm  13434  resmhm2  13435  resmhm2b  13436  mhmco  13437  gsumvallem2  13440  isgrpd2e  13467  grpinvf1o  13517  grpinvnzcl  13519  dfgrp3m  13546  mhmmnd  13567  ghmgrp  13569  mulgval  13573  mulgfng  13575  subgmulg  13639  issubg4m  13644  isnsg3  13658  nmzsubg  13661  ssnmz  13662  0nsg  13665  nsgid  13666  ghmnsgima  13719  ghmnsgpreima  13720  ghmf1  13724  kerf1ghm  13725  ghmf1o  13726  conjnmzb  13731  isabld  13750  ghmcmn  13778  ghmabl  13779  invghm  13780  srgfcl  13850  srglmhm  13870  srgrmhm  13871  iscrngd  13919  ringsrg  13924  unitabl  13994  rhmf1o  14045  rhmco  14051  ringelnzr  14064  subrngringnsg  14082  subrgcrng  14102  subrgnzr  14119  resrhm  14125  unitrrg  14144  lssneln0  14251  rnglidlmsgrp  14374  quscrng  14410  expghmap  14484  mulgghm2  14485  znf1o  14528  znidom  14534  znidomb  14535  psrbaglesuppg  14549  tgtopon  14653  distopon  14674  epttop  14677  resttopon  14758  resttopon2  14765  cnco  14808  lmss  14833  txtopon  14849  uptx  14861  txdis1cn  14865  hmeocnv  14894  hmeof1o2  14895  hmeores  14902  hmeoco  14903  idhmeo  14904  txhmeo  14906  txswaphmeo  14908  psmetxrge0  14919  isxmet2d  14935  metres2  14968  xmetresbl  15027  comet  15086  bdxmet  15088  bdmet  15089  tgioo  15141  mulc1cncf  15176  mulcncflem  15194  cnrehmeocntop  15197  cnopnap  15198  dedekindeu  15210  dedekindicclemicc  15219  ivthinclemlm  15221  ivthinclemum  15222  ivthinclemlopn  15223  ivthinclemlr  15224  ivthinclemuopn  15225  ivthinclemur  15226  ivthinclemloc  15228  ivthinc  15230  ivthreinc  15232  dvfgg  15275  dvcjbr  15295  dvcj  15296  dvfre  15297  elplyr  15327  plyreres  15351  rplogbval  15532  sgmnncl  15575  mpodvdsmulf1o  15577  mersenne  15584  perfectlem2  15587  lgsfcl2  15598  lgsval2lem  15602  lgsmod  15618  lgsdirprm  15626  lgsne0  15630  gausslemma2dlem0h  15648  gausslemma2dlem1a  15650  gausslemma2dlem1f1o  15652  gausslemma2dlem4  15656  lgseisenlem1  15662  lgseisenlem2  15663  lgsquadlem1  15669  lgsquadlem2  15670  lgsquad2lem2  15674  2sqlem8  15715  2sqlem9  15716  structiedg0val  15754  bj-charfundcALT  15944  bj-nnord  16093  bj-inf2vnlem1  16105  pwf1oexmid  16138  nnsf  16144  nninfall  16148  nninfself  16152  exmidsbthrlem  16163  qdencn  16168