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  2974  euind  2991  reuind  3009  eldifd  3208  eqssd  3242  ssrabdv  3304  elind  3390  dcun  3602  opm  4324  issod  4414  ordsucim  4596  onintonm  4613  ordtri2or2exmidlem  4622  en2lp  4650  ordwe  4672  sosng  4797  sotri2  5132  sotri3  5133  relssdmrn  5255  funun  5368  fnsng  5374  fnprg  5382  fntpg  5383  fntp  5384  fununi  5395  imain  5409  fnco  5437  f00  5525  f1ss  5545  f1ssr  5546  f1ssres  5548  f1f1orn  5591  foimacnv  5598  foun  5599  fun11iun  5601  sefvex  5656  dff3im  5788  fmpt  5793  ffnfv  5801  fmpt2d  5805  ffvresb  5806  fprg  5832  foco2  5889  fcof1  5919  fcofo  5920  fcof1o  5925  fliftf  5935  isoini2  5955  f1oiso  5962  moriotass  5997  fnoprabg  6117  f1ocnvd  6220  suppssfv  6226  suppssov1  6227  1stcof  6321  2ndcof  6322  1stconst  6381  2ndconst  6382  fo2ndf  6387  f1o2ndf1  6388  f1od2  6395  smores2  6455  tfrlem5  6475  tfrlemibfn  6489  tfr1onlembfn  6505  tfri1dALT  6512  tfrcllembfn  6518  nntri2  6657  eroveu  6790  elixpsn  6899  dom2lem  6940  xpf1o  7025  fidifsnen  7052  finexdc  7085  elssdc  7087  unfidisj  7107  f1finf1o  7137  fidcenumlemrks  7143  sbthlemi9  7155  supeuti  7184  infeuti  7219  casef1  7280  caseinl  7281  caseinr  7282  difinfsnlem  7289  ctmlemr  7298  ctm  7299  ctssdclemn0  7300  ctssdccl  7301  ctssdc  7303  enumctlemm  7304  nnnninf  7316  nninfwlpoimlemg  7365  en2other2  7397  exmidfodomrlemim  7402  pw1if  7433  pw1nel3  7439  dftap2  7460  cc2lem  7475  cc4f  7478  addclpi  7537  mulclpi  7538  nnppipi  7553  recmulnqg  7601  enq0ref  7643  nqnq0pi  7648  genipv  7719  addclpr  7747  nqprxx  7756  prmuloc  7776  mulclpr  7782  distrlem1prl  7792  distrlem1pru  7793  ltexprlempr  7818  ltexprlemrl  7820  ltexprlemru  7822  lteupri  7827  recexprlempr  7842  cauappcvgprlemm  7855  cauappcvgprlemopl  7856  cauappcvgprlemlol  7857  cauappcvgprlemopu  7858  cauappcvgprlemupu  7859  cauappcvgprlemloc  7862  cauappcvgprlemcl  7863  cauappcvgprlemladdfu  7864  cauappcvgprlemladdfl  7865  cauappcvgprlem2  7870  caucvgprlemm  7878  caucvgprlemopl  7879  caucvgprlemlol  7880  caucvgprlemopu  7881  caucvgprlemupu  7882  caucvgprlemloc  7885  caucvgprlemcl  7886  caucvgprlemladdfu  7887  caucvgprlem2  7890  caucvgprprlemml  7904  caucvgprprlemmu  7905  caucvgprprlemopl  7907  caucvgprprlemlol  7908  caucvgprprlemopu  7909  caucvgprprlemupu  7910  caucvgprprlemloc  7913  caucvgprprlemcl  7914  caucvgprprlem2  7920  suplocexprlemex  7932  suplocsrlem  8018  elrealeu  8039  rereceu  8099  axpre-suploclemres  8111  negf1o  8551  aptap  8820  receuap  8839  divvalap  8844  cju  9131  nn0ge2m1nn  9452  nnnegz  9472  elnnz  9479  elnn0z  9482  peano2z  9505  nn0n0n1ge2  9540  msqznn  9570  eluzaddi  9773  eluzsubi  9774  uzind4  9812  supinfneg  9819  infsupneg  9820  elnn1uz2  9831  uz2mulcl  9832  divfnzn  9845  nnrp  9888  rpaddcl  9902  rpmulcl  9903  rpdivcl  9904  rpgecl  9907  ge0p1rp  9910  elrpd  9918  ge0addcl  10206  ge0mulcl  10207  ge0xaddcl  10208  icoshftf1o  10216  peano2fzr  10262  uzsubsubfz  10272  fzsplit2  10275  elfznn  10279  fzss1  10288  fzss2  10289  fzp1elp1  10300  elfz1b  10315  elfz0fzfz0  10351  fz0fzelfz0  10352  difelfznle  10360  elfzofz  10388  fzosplitsnm1  10444  ubmelm1fzo  10461  fzofzp1b  10463  fzosplitsn  10468  zsupcllemstep  10479  zsupcl  10481  exbtwnz  10500  flqge0nn0  10543  flqge1nn  10544  zmodcl  10596  modqmuladdnn0  10620  modsumfzodifsn  10648  frec2uzf1od  10658  frec2uzisod  10659  frecuzrdgrrn  10660  frec2uzrdg  10661  frecuzrdgrcl  10662  frecuzrdgtcl  10664  frecuzrdgsuc  10666  frecuzrdgrclt  10667  frecuzrdgfunlem  10671  frecuzrdgtclt  10673  frecuzrdgsuctlem  10675  uzennn  10688  seq3fveq2  10727  seqfveq2g  10729  monoord  10737  iseqf1olemqcl  10751  iseqf1olemnab  10753  iseqf1olemab  10754  iseqf1olemqf1o  10758  seq3f1olemqsumkj  10763  seq3f1olemqsumk  10764  seq3id2  10778  exp3val  10793  expcl2lemap  10803  expclzaplem  10815  expge0  10827  expge1  10828  zsqcl2  10869  bcval4  11004  bcn1  11010  bccl2  11020  hashennnuni  11031  hashunlem  11057  hashdifpr  11074  zfz1isolem1  11094  seq3coll  11096  iswrdiz  11110  ccatsymb  11169  ccatrn  11176  ccat2s1fvwd  11214  swrds1  11239  swrdccat2  11242  swrdccatin2  11300  pfxccatin12lem2  11302  pfxccatin12lem3  11303  pfxccatin12  11304  pfxccat3  11305  pfxccat3a  11309  shftfn  11375  shftf  11381  recvguniq  11546  resqrexlemdecn  11563  rersqreu  11579  nn0abscl  11636  nnabscl  11651  abs2dif  11657  nn0maxcl  11776  climuni  11844  2clim  11852  climcn2  11860  summodclem2a  11932  fsum3  11938  fsum3cvg3  11947  fsumcl2lem  11949  fsumadd  11957  fisum0diag2  11998  fsummulc2  11999  fsumge0  12010  geolim2  12063  cvgratnnlemabsle  12078  cvgratz  12083  mertenslemi1  12086  prodmodclem3  12126  prodmodclem2a  12127  fprodeq0  12168  fprodge0  12188  eff2  12231  tanvalap  12259  zdvdsdc  12363  fzo0dvdseq  12408  oexpneg  12428  oddge22np1  12432  evennn02n  12433  evennn2n  12434  nno  12457  divalglemeunn  12472  divalglemex  12473  divalglemeuneg  12474  divalg  12475  bitsfzolem  12505  bitsinv1lem  12512  divgcdz  12532  bezoutlemmain  12559  bezoutlemmo  12567  bezoutlemeu  12568  bezoutlemle  12569  sqgcd  12590  uzwodc  12598  nninfctlemfo  12601  eucalgval2  12615  eucalglt  12619  lcmneg  12636  lcmgcdlem  12639  ncoprmgcdne1b  12651  prmind2  12682  prmdc  12692  sqnprm  12698  isprm5lem  12703  isprm5  12704  isprm6  12709  sqrt2irrlem  12723  pw2dvdseu  12730  sqpweven  12737  2sqpwodd  12738  sqrt2irrap  12742  qgt0numnn  12761  phicl2  12776  hashdvds  12783  crth  12786  phimullem  12787  eulerthlem1  12789  eulerthlemh  12793  eulerthlemth  12794  hashgcdlem  12800  oddprm  12822  pythagtriplem6  12833  pythagtriplem11  12837  pythagtriplem13  12839  pythagtriplem19  12845  pclem0  12849  pcpremul  12856  pceu  12858  pc2dvds  12893  difsqpwdvds  12901  pcadd  12903  pockthlem  12919  pockthg  12920  1arith  12930  4sqlemffi  12959  4sqlem11  12964  4sqlem12  12965  4sqlem13m  12966  4sqlem14  12967  4sqlem17  12970  oddennn  13003  evenennn  13004  ennnfoneleminc  13022  ennnfonelemf1  13029  ennnfonelemen  13032  exmidunben  13037  ctinf  13041  ctiunctlemfo  13050  nninfdclemlt  13062  nninfdclemf1  13063  ptex  13337  imasaddfnlemg  13387  imasaddflemg  13389  mgmsscl  13434  sgrp0  13483  sgrp1  13484  hashfinmndnn  13505  ismndd  13510  mndpfo  13511  mhmf1o  13543  0mhm  13559  resmhm  13560  resmhm2  13561  resmhm2b  13562  mhmco  13563  gsumvallem2  13566  isgrpd2e  13593  grpinvf1o  13643  grpinvnzcl  13645  dfgrp3m  13672  mhmmnd  13693  ghmgrp  13695  mulgval  13699  mulgfng  13701  subgmulg  13765  issubg4m  13770  isnsg3  13784  nmzsubg  13787  ssnmz  13788  0nsg  13791  nsgid  13792  ghmnsgima  13845  ghmnsgpreima  13846  ghmf1  13850  kerf1ghm  13851  ghmf1o  13852  conjnmzb  13857  isabld  13876  ghmcmn  13904  ghmabl  13905  invghm  13906  srgfcl  13976  srglmhm  13996  srgrmhm  13997  iscrngd  14045  ringsrg  14050  unitabl  14121  rhmf1o  14172  rhmco  14178  ringelnzr  14191  subrngringnsg  14209  subrgcrng  14229  subrgnzr  14246  resrhm  14252  unitrrg  14271  lssneln0  14378  rnglidlmsgrp  14501  quscrng  14537  expghmap  14611  mulgghm2  14612  znf1o  14655  znidom  14661  znidomb  14662  psrbaglesuppg  14676  tgtopon  14780  distopon  14801  epttop  14804  resttopon  14885  resttopon2  14892  cnco  14935  lmss  14960  txtopon  14976  uptx  14988  txdis1cn  14992  hmeocnv  15021  hmeof1o2  15022  hmeores  15029  hmeoco  15030  idhmeo  15031  txhmeo  15033  txswaphmeo  15035  psmetxrge0  15046  isxmet2d  15062  metres2  15095  xmetresbl  15154  comet  15213  bdxmet  15215  bdmet  15216  tgioo  15268  mulc1cncf  15303  mulcncflem  15321  cnrehmeocntop  15324  cnopnap  15325  dedekindeu  15337  dedekindicclemicc  15346  ivthinclemlm  15348  ivthinclemum  15349  ivthinclemlopn  15350  ivthinclemlr  15351  ivthinclemuopn  15352  ivthinclemur  15353  ivthinclemloc  15355  ivthinc  15357  ivthreinc  15359  dvfgg  15402  dvcjbr  15422  dvcj  15423  dvfre  15424  elplyr  15454  plyreres  15478  rplogbval  15659  sgmnncl  15702  mpodvdsmulf1o  15704  mersenne  15711  perfectlem2  15714  lgsfcl2  15725  lgsval2lem  15729  lgsmod  15745  lgsdirprm  15753  lgsne0  15757  gausslemma2dlem0h  15775  gausslemma2dlem1a  15777  gausslemma2dlem1f1o  15779  gausslemma2dlem4  15783  lgseisenlem1  15789  lgseisenlem2  15790  lgsquadlem1  15796  lgsquadlem2  15797  lgsquad2lem2  15801  2sqlem8  15842  2sqlem9  15843  structiedg0val  15881  ausgrumgrien  16009  usgredgreu  16055  uspgredg2vtxeu  16057  uspgredg2v  16060  usgredg2v  16063  usgr1e  16080  trlres  16185  clwwlkbp  16190  clwwlkccatlem  16195  s2elclwwlknon2  16231  clwwlknonex2lem2  16233  clwwlknonex2e  16235  bj-charfundcALT  16340  bj-nnord  16489  bj-inf2vnlem1  16501  pwf1oexmid  16536  nnsf  16543  nninfall  16547  nninfself  16551  exmidsbthrlem  16562  qdencn  16567