Theorem sylanbrc 409

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 301	. 2 |- ( ph -> ( ps /\ ch ) )
4		sylanbrc.3	. 2 |- ( th <-> ( ps /\ ch ) )
5	3, 4	sylibr 133	1 |- ( ph -> th )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  sb2  1704  sbequ1  1705  sbidm  1786  eqeu  2799  euind  2816  reuind  2834  eldifd  3023  eqssd  3056  ssrabdv  3115  elind  3200  dcun  3412  opm  4085  issod  4170  ordsucim  4345  onintonm  4362  ordtri2or2exmidlem  4370  en2lp  4398  ordwe  4419  sosng  4540  sotri2  4862  sotri3  4863  relssdmrn  4985  funun  5092  fnsng  5095  fnprg  5103  fntpg  5104  fntp  5105  fununi  5116  imain  5130  fnco  5156  f00  5237  f1ss  5257  f1ssr  5258  f1ssres  5260  f1f1orn  5299  foimacnv  5306  foun  5307  fun11iun  5309  sefvex  5361  dff3im  5483  fmpt  5488  ffnfv  5495  fmpt2d  5499  ffvresb  5500  fprg  5519  foco2  5571  fcof1  5600  fcofo  5601  fcof1o  5606  fliftf  5616  isoini2  5636  f1oiso  5643  moriotass  5674  fnoprabg  5784  f1ocnvd  5884  suppssfv  5890  suppssov1  5891  1stcof  5972  2ndcof  5973  1stconst  6024  2ndconst  6025  fo2ndf  6030  f1o2ndf1  6031  f1od2  6038  smores2  6097  tfrlem5  6117  tfrlemibfn  6131  tfr1onlembfn  6147  tfri1dALT  6154  tfrcllembfn  6160  nntri2  6295  eroveu  6423  elixpsn  6532  dom2lem  6569  xpf1o  6640  fidifsnen  6666  finexdc  6698  unfidisj  6712  f1finf1o  6736  fidcenumlemrks  6742  sbthlemi9  6754  supeuti  6769  infeuti  6804  casef1  6861  caseinl  6862  ctmlemr  6870  ctm  6871  enumctlemm  6872  nnnninf  6894  en2other2  6919  exmidfodomrlemim  6924  addclpi  6983  mulclpi  6984  nnppipi  6999  recmulnqg  7047  enq0ref  7089  nqnq0pi  7094  genipv  7165  addclpr  7193  nqprxx  7202  prmuloc  7222  mulclpr  7228  distrlem1prl  7238  distrlem1pru  7239  ltexprlempr  7264  ltexprlemrl  7266  ltexprlemru  7268  lteupri  7273  recexprlempr  7288  cauappcvgprlemm  7301  cauappcvgprlemopl  7302  cauappcvgprlemlol  7303  cauappcvgprlemopu  7304  cauappcvgprlemupu  7305  cauappcvgprlemloc  7308  cauappcvgprlemcl  7309  cauappcvgprlemladdfu  7310  cauappcvgprlemladdfl  7311  cauappcvgprlem2  7316  caucvgprlemm  7324  caucvgprlemopl  7325  caucvgprlemlol  7326  caucvgprlemopu  7327  caucvgprlemupu  7328  caucvgprlemloc  7331  caucvgprlemcl  7332  caucvgprlemladdfu  7333  caucvgprlem2  7336  caucvgprprlemml  7350  caucvgprprlemmu  7351  caucvgprprlemopl  7353  caucvgprprlemlol  7354  caucvgprprlemopu  7355  caucvgprprlemupu  7356  caucvgprprlemloc  7359  caucvgprprlemcl  7360  caucvgprprlem2  7366  elrealeu  7464  rereceu  7521  negf1o  7957  receuap  8235  divvalap  8238  cju  8519  nn0ge2m1nn  8831  nnnegz  8851  elnnz  8858  elnn0z  8861  peano2z  8884  nn0n0n1ge2  8915  msqznn  8945  eluzaddi  9144  eluzsubi  9145  uzind4  9175  supinfneg  9182  infsupneg  9183  elnn1uz2  9193  uz2mulcl  9194  divfnzn  9205  nnrp  9242  rpaddcl  9256  rpmulcl  9257  rpdivcl  9258  rpgecl  9261  ge0p1rp  9264  elrpd  9270  ge0addcl  9547  ge0mulcl  9548  ge0xaddcl  9549  icoshftf1o  9557  peano2fzr  9600  uzsubsubfz  9610  fzsplit2  9613  elfznn  9617  fzss1  9626  fzss2  9627  fzp1elp1  9638  elfz1b  9653  elfz0fzfz0  9686  fz0fzelfz0  9687  difelfznle  9695  elfzofz  9722  fzosplitsnm1  9769  ubmelm1fzo  9786  fzofzp1b  9788  fzosplitsn  9793  exbtwnz  9811  flqge0nn0  9849  flqge1nn  9850  zmodcl  9900  modqmuladdnn0  9924  modsumfzodifsn  9952  frec2uzf1od  9962  frec2uzisod  9963  frecuzrdgrrn  9964  frec2uzrdg  9965  frecuzrdgrcl  9966  frecuzrdgtcl  9968  frecuzrdgsuc  9970  frecuzrdgrclt  9971  frecuzrdgfunlem  9975  frecuzrdgtclt  9977  frecuzrdgsuctlem  9979  seq3fveq2  10034  monoord  10042  iseqf1olemqcl  10052  iseqf1olemnab  10054  iseqf1olemab  10055  iseqf1olemqf1o  10059  seq3f1olemqsumkj  10064  seq3f1olemqsumk  10065  seq3id2  10075  exp3val  10088  expcl2lemap  10098  expclzaplem  10110  expge0  10122  expge1  10123  zsqcl2  10163  bcval4  10291  bcn1  10297  bccl2  10307  hashennnuni  10318  hashunlem  10343  hashdifpr  10359  zfz1isolem1  10376  seq3coll  10378  shftfn  10389  shftf  10395  recvguniq  10559  resqrexlemdecn  10576  rersqreu  10592  nn0abscl  10649  nnabscl  10664  abs2dif  10670  climuni  10852  2clim  10860  climcn2  10868  summodclem2a  10939  fsum3  10945  fsum3cvg3  10954  fsumcl2lem  10956  fsumadd  10964  fisum0diag2  11005  fsummulc2  11006  fsumge0  11017  geolim2  11070  cvgratnnlemabsle  11085  cvgratz  11090  mertenslemi1  11093  eff2  11134  tanvalap  11163  zdvdsdc  11259  fzo0dvdseq  11300  oexpneg  11319  oddge22np1  11323  evennn02n  11324  evennn2n  11325  nno  11348  divalglemeunn  11363  divalglemex  11364  divalglemeuneg  11365  divalg  11366  zsupcllemstep  11383  zsupcl  11385  divgcdz  11405  bezoutlemmain  11429  bezoutlemmo  11437  bezoutlemeu  11438  bezoutlemle  11439  sqgcd  11460  eucalgval2  11477  eucalglt  11481  lcmcllem  11491  lcmledvds  11494  lcmneg  11498  lcmgcdlem  11501  ncoprmgcdne1b  11513  prmind2  11544  sqnprm  11559  isprm6  11568  sqrt2irrlem  11582  pw2dvdseu  11588  sqpweven  11595  2sqpwodd  11596  sqrt2irrap  11600  qgt0numnn  11619  phicl2  11632  hashdvds  11639  crth  11642  phimullem  11643  hashgcdlem  11645  oddennn  11647  evenennn  11648  tgtopon  11933  distopon  11954  epttop  11957  resttopon  12038  resttopon2  12045  cnco  12087  lmss  12112  psmetxrge0  12133  isxmet2d  12149  metres2  12182  xmetresbl  12241  comet  12300  bdxmet  12302  bdmet  12303  tgioo  12335  mulc1cncf  12357  bj-nnord  12565  bj-inf2vnlem1  12577  nnsf  12604  nninfall  12609  nninfself  12614  exmidsbthrlem  12621  qdencn  12624