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:  sb2  1767  sbequ1  1768  sbidm  1851  eqeu  2908  euind  2925  reuind  2943  eldifd  3140  eqssd  3173  ssrabdv  3235  elind  3321  dcun  3534  opm  4235  issod  4320  ordsucim  4500  onintonm  4517  ordtri2or2exmidlem  4526  en2lp  4554  ordwe  4576  sosng  4700  sotri2  5027  sotri3  5028  relssdmrn  5150  funun  5261  fnsng  5264  fnprg  5272  fntpg  5273  fntp  5274  fununi  5285  imain  5299  fnco  5325  f00  5408  f1ss  5428  f1ssr  5429  f1ssres  5431  f1f1orn  5473  foimacnv  5480  foun  5481  fun11iun  5483  sefvex  5537  dff3im  5662  fmpt  5667  ffnfv  5675  fmpt2d  5679  ffvresb  5680  fprg  5700  foco2  5755  fcof1  5784  fcofo  5785  fcof1o  5790  fliftf  5800  isoini2  5820  f1oiso  5827  moriotass  5859  fnoprabg  5976  f1ocnvd  6073  suppssfv  6079  suppssov1  6080  1stcof  6164  2ndcof  6165  1stconst  6222  2ndconst  6223  fo2ndf  6228  f1o2ndf1  6229  f1od2  6236  smores2  6295  tfrlem5  6315  tfrlemibfn  6329  tfr1onlembfn  6345  tfri1dALT  6352  tfrcllembfn  6358  nntri2  6495  eroveu  6626  elixpsn  6735  dom2lem  6772  xpf1o  6844  fidifsnen  6870  finexdc  6902  unfidisj  6921  f1finf1o  6946  fidcenumlemrks  6952  sbthlemi9  6964  supeuti  6993  infeuti  7028  casef1  7089  caseinl  7090  caseinr  7091  difinfsnlem  7098  ctmlemr  7107  ctm  7108  ctssdclemn0  7109  ctssdccl  7110  ctssdc  7112  enumctlemm  7113  nnnninf  7124  nninfwlpoimlemg  7173  en2other2  7195  exmidfodomrlemim  7200  pw1nel3  7230  dftap2  7250  cc2lem  7265  cc4f  7268  addclpi  7326  mulclpi  7327  nnppipi  7342  recmulnqg  7390  enq0ref  7432  nqnq0pi  7437  genipv  7508  addclpr  7536  nqprxx  7545  prmuloc  7565  mulclpr  7571  distrlem1prl  7581  distrlem1pru  7582  ltexprlempr  7607  ltexprlemrl  7609  ltexprlemru  7611  lteupri  7616  recexprlempr  7631  cauappcvgprlemm  7644  cauappcvgprlemopl  7645  cauappcvgprlemlol  7646  cauappcvgprlemopu  7647  cauappcvgprlemupu  7648  cauappcvgprlemloc  7651  cauappcvgprlemcl  7652  cauappcvgprlemladdfu  7653  cauappcvgprlemladdfl  7654  cauappcvgprlem2  7659  caucvgprlemm  7667  caucvgprlemopl  7668  caucvgprlemlol  7669  caucvgprlemopu  7670  caucvgprlemupu  7671  caucvgprlemloc  7674  caucvgprlemcl  7675  caucvgprlemladdfu  7676  caucvgprlem2  7679  caucvgprprlemml  7693  caucvgprprlemmu  7694  caucvgprprlemopl  7696  caucvgprprlemlol  7697  caucvgprprlemopu  7698  caucvgprprlemupu  7699  caucvgprprlemloc  7702  caucvgprprlemcl  7703  caucvgprprlem2  7709  suplocexprlemex  7721  suplocsrlem  7807  elrealeu  7828  rereceu  7888  axpre-suploclemres  7900  negf1o  8339  aptap  8607  receuap  8626  divvalap  8631  cju  8918  nn0ge2m1nn  9236  nnnegz  9256  elnnz  9263  elnn0z  9266  peano2z  9289  nn0n0n1ge2  9323  msqznn  9353  eluzaddi  9554  eluzsubi  9555  uzind4  9588  supinfneg  9595  infsupneg  9596  elnn1uz2  9607  uz2mulcl  9608  divfnzn  9621  nnrp  9663  rpaddcl  9677  rpmulcl  9678  rpdivcl  9679  rpgecl  9682  ge0p1rp  9685  elrpd  9693  ge0addcl  9981  ge0mulcl  9982  ge0xaddcl  9983  icoshftf1o  9991  peano2fzr  10037  uzsubsubfz  10047  fzsplit2  10050  elfznn  10054  fzss1  10063  fzss2  10064  fzp1elp1  10075  elfz1b  10090  elfz0fzfz0  10126  fz0fzelfz0  10127  difelfznle  10135  elfzofz  10162  fzosplitsnm1  10209  ubmelm1fzo  10226  fzofzp1b  10228  fzosplitsn  10233  exbtwnz  10251  flqge0nn0  10293  flqge1nn  10294  zmodcl  10344  modqmuladdnn0  10368  modsumfzodifsn  10396  frec2uzf1od  10406  frec2uzisod  10407  frecuzrdgrrn  10408  frec2uzrdg  10409  frecuzrdgrcl  10410  frecuzrdgtcl  10412  frecuzrdgsuc  10414  frecuzrdgrclt  10415  frecuzrdgfunlem  10419  frecuzrdgtclt  10421  frecuzrdgsuctlem  10423  uzennn  10436  seq3fveq2  10469  monoord  10476  iseqf1olemqcl  10486  iseqf1olemnab  10488  iseqf1olemab  10489  iseqf1olemqf1o  10493  seq3f1olemqsumkj  10498  seq3f1olemqsumk  10499  seq3id2  10509  exp3val  10522  expcl2lemap  10532  expclzaplem  10544  expge0  10556  expge1  10557  zsqcl2  10598  bcval4  10732  bcn1  10738  bccl2  10748  hashennnuni  10759  hashunlem  10784  hashdifpr  10800  zfz1isolem1  10820  seq3coll  10822  shftfn  10833  shftf  10839  recvguniq  11004  resqrexlemdecn  11021  rersqreu  11037  nn0abscl  11094  nnabscl  11109  abs2dif  11115  climuni  11301  2clim  11309  climcn2  11317  summodclem2a  11389  fsum3  11395  fsum3cvg3  11404  fsumcl2lem  11406  fsumadd  11414  fisum0diag2  11455  fsummulc2  11456  fsumge0  11467  geolim2  11520  cvgratnnlemabsle  11535  cvgratz  11540  mertenslemi1  11543  prodmodclem3  11583  prodmodclem2a  11584  fprodeq0  11625  fprodge0  11645  eff2  11688  tanvalap  11716  zdvdsdc  11819  fzo0dvdseq  11863  oexpneg  11882  oddge22np1  11886  evennn02n  11887  evennn2n  11888  nno  11911  divalglemeunn  11926  divalglemex  11927  divalglemeuneg  11928  divalg  11929  zsupcllemstep  11946  zsupcl  11948  divgcdz  11972  bezoutlemmain  11999  bezoutlemmo  12007  bezoutlemeu  12008  bezoutlemle  12009  sqgcd  12030  uzwodc  12038  eucalgval2  12053  eucalglt  12057  lcmcllem  12067  lcmledvds  12070  lcmneg  12074  lcmgcdlem  12077  ncoprmgcdne1b  12089  prmind2  12120  prmdc  12130  sqnprm  12136  isprm5lem  12141  isprm5  12142  isprm6  12147  sqrt2irrlem  12161  pw2dvdseu  12168  sqpweven  12175  2sqpwodd  12176  sqrt2irrap  12180  qgt0numnn  12199  phicl2  12214  hashdvds  12221  crth  12224  phimullem  12225  eulerthlem1  12227  eulerthlemh  12231  eulerthlemth  12232  hashgcdlem  12238  oddprm  12259  pythagtriplem6  12270  pythagtriplem11  12274  pythagtriplem13  12276  pythagtriplem19  12282  pclem0  12286  pcpremul  12293  pceu  12295  pc2dvds  12329  difsqpwdvds  12337  pcadd  12339  pockthlem  12354  pockthg  12355  1arith  12365  oddennn  12393  evenennn  12394  ennnfoneleminc  12412  ennnfonelemf1  12419  ennnfonelemen  12422  exmidunben  12427  ctinf  12431  ctiunctlemfo  12440  nninfdclemlt  12452  nninfdclemf1  12453  ptex  12713  imasaddfnlemg  12735  imasaddflemg  12737  mgmsscl  12780  sgrp0  12815  sgrp1  12816  hashfinmndnn  12833  ismndd  12838  mndpfo  12839  mhmf1o  12861  0mhm  12873  mhmco  12874  isgrpd2e  12896  grpinvf1o  12940  grpinvnzcl  12942  dfgrp3m  12969  mhmmnd  12980  ghmgrp  12982  mulgval  12986  mulgfng  12987  subgmulg  13048  issubg4m  13053  isnsg3  13067  nmzsubg  13070  ssnmz  13071  0nsg  13074  nsgid  13075  isabld  13102  srgfcl  13156  srglmhm  13176  srgrmhm  13177  iscrngd  13221  ringsrg  13224  unitabl  13286  ringelnzr  13328  subrgcrng  13346  subrgnzr  13363  tgtopon  13569  distopon  13590  epttop  13593  resttopon  13674  resttopon2  13681  cnco  13724  lmss  13749  txtopon  13765  uptx  13777  txdis1cn  13781  hmeocnv  13810  hmeof1o2  13811  hmeores  13818  hmeoco  13819  idhmeo  13820  txhmeo  13822  txswaphmeo  13824  psmetxrge0  13835  isxmet2d  13851  metres2  13884  xmetresbl  13943  comet  14002  bdxmet  14004  bdmet  14005  tgioo  14049  mulc1cncf  14079  mulcncflem  14093  cnrehmeocntop  14096  cnopnap  14097  dedekindeu  14104  dedekindicclemicc  14113  ivthinclemlm  14115  ivthinclemum  14116  ivthinclemlopn  14117  ivthinclemlr  14118  ivthinclemuopn  14119  ivthinclemur  14120  ivthinclemloc  14122  ivthinc  14124  dvfgg  14160  dvcjbr  14175  dvcj  14176  dvfre  14177  rplogbval  14366  lgsfcl2  14410  lgsval2lem  14414  lgsmod  14430  lgsdirprm  14438  lgsne0  14442  lgseisenlem1  14453  lgseisenlem2  14454  2sqlem8  14473  2sqlem9  14474  bj-charfundcALT  14564  bj-nnord  14713  bj-inf2vnlem1  14725  pwf1oexmid  14752  nnsf  14757  nninfall  14761  nninfself  14765  exmidsbthrlem  14773  qdencn  14778