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  934  sb2  1789  sbequ1  1790  sbidm  1873  eqeu  2942  euind  2959  reuind  2977  eldifd  3175  eqssd  3209  ssrabdv  3271  elind  3357  dcun  3569  opm  4277  issod  4365  ordsucim  4547  onintonm  4564  ordtri2or2exmidlem  4573  en2lp  4601  ordwe  4623  sosng  4747  sotri2  5079  sotri3  5080  relssdmrn  5202  funun  5314  fnsng  5320  fnprg  5328  fntpg  5329  fntp  5330  fununi  5341  imain  5355  fnco  5383  f00  5466  f1ss  5486  f1ssr  5487  f1ssres  5489  f1f1orn  5532  foimacnv  5539  foun  5540  fun11iun  5542  sefvex  5596  dff3im  5724  fmpt  5729  ffnfv  5737  fmpt2d  5741  ffvresb  5742  fprg  5766  foco2  5821  fcof1  5851  fcofo  5852  fcof1o  5857  fliftf  5867  isoini2  5887  f1oiso  5894  moriotass  5927  fnoprabg  6045  f1ocnvd  6147  suppssfv  6153  suppssov1  6154  1stcof  6248  2ndcof  6249  1stconst  6306  2ndconst  6307  fo2ndf  6312  f1o2ndf1  6313  f1od2  6320  smores2  6379  tfrlem5  6399  tfrlemibfn  6413  tfr1onlembfn  6429  tfri1dALT  6436  tfrcllembfn  6442  nntri2  6579  eroveu  6712  elixpsn  6821  dom2lem  6862  xpf1o  6940  fidifsnen  6966  finexdc  6998  unfidisj  7018  f1finf1o  7048  fidcenumlemrks  7054  sbthlemi9  7066  supeuti  7095  infeuti  7130  casef1  7191  caseinl  7192  caseinr  7193  difinfsnlem  7200  ctmlemr  7209  ctm  7210  ctssdclemn0  7211  ctssdccl  7212  ctssdc  7214  enumctlemm  7215  nnnninf  7227  nninfwlpoimlemg  7276  en2other2  7303  exmidfodomrlemim  7308  pw1nel3  7342  dftap2  7362  cc2lem  7377  cc4f  7380  addclpi  7439  mulclpi  7440  nnppipi  7455  recmulnqg  7503  enq0ref  7545  nqnq0pi  7550  genipv  7621  addclpr  7649  nqprxx  7658  prmuloc  7678  mulclpr  7684  distrlem1prl  7694  distrlem1pru  7695  ltexprlempr  7720  ltexprlemrl  7722  ltexprlemru  7724  lteupri  7729  recexprlempr  7744  cauappcvgprlemm  7757  cauappcvgprlemopl  7758  cauappcvgprlemlol  7759  cauappcvgprlemopu  7760  cauappcvgprlemupu  7761  cauappcvgprlemloc  7764  cauappcvgprlemcl  7765  cauappcvgprlemladdfu  7766  cauappcvgprlemladdfl  7767  cauappcvgprlem2  7772  caucvgprlemm  7780  caucvgprlemopl  7781  caucvgprlemlol  7782  caucvgprlemopu  7783  caucvgprlemupu  7784  caucvgprlemloc  7787  caucvgprlemcl  7788  caucvgprlemladdfu  7789  caucvgprlem2  7792  caucvgprprlemml  7806  caucvgprprlemmu  7807  caucvgprprlemopl  7809  caucvgprprlemlol  7810  caucvgprprlemopu  7811  caucvgprprlemupu  7812  caucvgprprlemloc  7815  caucvgprprlemcl  7816  caucvgprprlem2  7822  suplocexprlemex  7834  suplocsrlem  7920  elrealeu  7941  rereceu  8001  axpre-suploclemres  8013  negf1o  8453  aptap  8722  receuap  8741  divvalap  8746  cju  9033  nn0ge2m1nn  9354  nnnegz  9374  elnnz  9381  elnn0z  9384  peano2z  9407  nn0n0n1ge2  9442  msqznn  9472  eluzaddi  9674  eluzsubi  9675  uzind4  9708  supinfneg  9715  infsupneg  9716  elnn1uz2  9727  uz2mulcl  9728  divfnzn  9741  nnrp  9784  rpaddcl  9798  rpmulcl  9799  rpdivcl  9800  rpgecl  9803  ge0p1rp  9806  elrpd  9814  ge0addcl  10102  ge0mulcl  10103  ge0xaddcl  10104  icoshftf1o  10112  peano2fzr  10158  uzsubsubfz  10168  fzsplit2  10171  elfznn  10175  fzss1  10184  fzss2  10185  fzp1elp1  10196  elfz1b  10211  elfz0fzfz0  10247  fz0fzelfz0  10248  difelfznle  10256  elfzofz  10284  fzosplitsnm1  10336  ubmelm1fzo  10353  fzofzp1b  10355  fzosplitsn  10360  zsupcllemstep  10370  zsupcl  10372  exbtwnz  10391  flqge0nn0  10434  flqge1nn  10435  zmodcl  10487  modqmuladdnn0  10511  modsumfzodifsn  10539  frec2uzf1od  10549  frec2uzisod  10550  frecuzrdgrrn  10551  frec2uzrdg  10552  frecuzrdgrcl  10553  frecuzrdgtcl  10555  frecuzrdgsuc  10557  frecuzrdgrclt  10558  frecuzrdgfunlem  10562  frecuzrdgtclt  10564  frecuzrdgsuctlem  10566  uzennn  10579  seq3fveq2  10618  seqfveq2g  10620  monoord  10628  iseqf1olemqcl  10642  iseqf1olemnab  10644  iseqf1olemab  10645  iseqf1olemqf1o  10649  seq3f1olemqsumkj  10654  seq3f1olemqsumk  10655  seq3id2  10669  exp3val  10684  expcl2lemap  10694  expclzaplem  10706  expge0  10718  expge1  10719  zsqcl2  10760  bcval4  10895  bcn1  10901  bccl2  10911  hashennnuni  10922  hashunlem  10947  hashdifpr  10963  zfz1isolem1  10983  seq3coll  10985  iswrdiz  10999  ccatsymb  11056  ccatrn  11063  shftfn  11106  shftf  11112  recvguniq  11277  resqrexlemdecn  11294  rersqreu  11310  nn0abscl  11367  nnabscl  11382  abs2dif  11388  nn0maxcl  11507  climuni  11575  2clim  11583  climcn2  11591  summodclem2a  11663  fsum3  11669  fsum3cvg3  11678  fsumcl2lem  11680  fsumadd  11688  fisum0diag2  11729  fsummulc2  11730  fsumge0  11741  geolim2  11794  cvgratnnlemabsle  11809  cvgratz  11814  mertenslemi1  11817  prodmodclem3  11857  prodmodclem2a  11858  fprodeq0  11899  fprodge0  11919  eff2  11962  tanvalap  11990  zdvdsdc  12094  fzo0dvdseq  12139  oexpneg  12159  oddge22np1  12163  evennn02n  12164  evennn2n  12165  nno  12188  divalglemeunn  12203  divalglemex  12204  divalglemeuneg  12205  divalg  12206  bitsfzolem  12236  bitsinv1lem  12243  divgcdz  12263  bezoutlemmain  12290  bezoutlemmo  12298  bezoutlemeu  12299  bezoutlemle  12300  sqgcd  12321  uzwodc  12329  nninfctlemfo  12332  eucalgval2  12346  eucalglt  12350  lcmneg  12367  lcmgcdlem  12370  ncoprmgcdne1b  12382  prmind2  12413  prmdc  12423  sqnprm  12429  isprm5lem  12434  isprm5  12435  isprm6  12440  sqrt2irrlem  12454  pw2dvdseu  12461  sqpweven  12468  2sqpwodd  12469  sqrt2irrap  12473  qgt0numnn  12492  phicl2  12507  hashdvds  12514  crth  12517  phimullem  12518  eulerthlem1  12520  eulerthlemh  12524  eulerthlemth  12525  hashgcdlem  12531  oddprm  12553  pythagtriplem6  12564  pythagtriplem11  12568  pythagtriplem13  12570  pythagtriplem19  12576  pclem0  12580  pcpremul  12587  pceu  12589  pc2dvds  12624  difsqpwdvds  12632  pcadd  12634  pockthlem  12650  pockthg  12651  1arith  12661  4sqlemffi  12690  4sqlem11  12695  4sqlem12  12696  4sqlem13m  12697  4sqlem14  12698  4sqlem17  12701  oddennn  12734  evenennn  12735  ennnfoneleminc  12753  ennnfonelemf1  12760  ennnfonelemen  12763  exmidunben  12768  ctinf  12772  ctiunctlemfo  12781  nninfdclemlt  12793  nninfdclemf1  12794  ptex  13067  imasaddfnlemg  13117  imasaddflemg  13119  mgmsscl  13164  sgrp0  13213  sgrp1  13214  hashfinmndnn  13235  ismndd  13240  mndpfo  13241  mhmf1o  13273  0mhm  13289  resmhm  13290  resmhm2  13291  resmhm2b  13292  mhmco  13293  gsumvallem2  13296  isgrpd2e  13323  grpinvf1o  13373  grpinvnzcl  13375  dfgrp3m  13402  mhmmnd  13423  ghmgrp  13425  mulgval  13429  mulgfng  13431  subgmulg  13495  issubg4m  13500  isnsg3  13514  nmzsubg  13517  ssnmz  13518  0nsg  13521  nsgid  13522  ghmnsgima  13575  ghmnsgpreima  13576  ghmf1  13580  kerf1ghm  13581  ghmf1o  13582  conjnmzb  13587  isabld  13606  ghmcmn  13634  ghmabl  13635  invghm  13636  srgfcl  13706  srglmhm  13726  srgrmhm  13727  iscrngd  13775  ringsrg  13780  unitabl  13850  rhmf1o  13901  rhmco  13907  ringelnzr  13920  subrngringnsg  13938  subrgcrng  13958  subrgnzr  13975  resrhm  13981  unitrrg  14000  lssneln0  14107  rnglidlmsgrp  14230  quscrng  14266  expghmap  14340  mulgghm2  14341  znf1o  14384  znidom  14390  znidomb  14391  psrbaglesuppg  14405  tgtopon  14509  distopon  14530  epttop  14533  resttopon  14614  resttopon2  14621  cnco  14664  lmss  14689  txtopon  14705  uptx  14717  txdis1cn  14721  hmeocnv  14750  hmeof1o2  14751  hmeores  14758  hmeoco  14759  idhmeo  14760  txhmeo  14762  txswaphmeo  14764  psmetxrge0  14775  isxmet2d  14791  metres2  14824  xmetresbl  14883  comet  14942  bdxmet  14944  bdmet  14945  tgioo  14997  mulc1cncf  15032  mulcncflem  15050  cnrehmeocntop  15053  cnopnap  15054  dedekindeu  15066  dedekindicclemicc  15075  ivthinclemlm  15077  ivthinclemum  15078  ivthinclemlopn  15079  ivthinclemlr  15080  ivthinclemuopn  15081  ivthinclemur  15082  ivthinclemloc  15084  ivthinc  15086  ivthreinc  15088  dvfgg  15131  dvcjbr  15151  dvcj  15152  dvfre  15153  elplyr  15183  plyreres  15207  rplogbval  15388  sgmnncl  15431  mpodvdsmulf1o  15433  mersenne  15440  perfectlem2  15443  lgsfcl2  15454  lgsval2lem  15458  lgsmod  15474  lgsdirprm  15482  lgsne0  15486  gausslemma2dlem0h  15504  gausslemma2dlem1a  15506  gausslemma2dlem1f1o  15508  gausslemma2dlem4  15512  lgseisenlem1  15518  lgseisenlem2  15519  lgsquadlem1  15525  lgsquadlem2  15526  lgsquad2lem2  15530  2sqlem8  15571  2sqlem9  15572  structiedg0val  15608  bj-charfundcALT  15707  bj-nnord  15856  bj-inf2vnlem1  15868  pwf1oexmid  15898  nnsf  15904  nninfall  15908  nninfself  15912  exmidsbthrlem  15923  qdencn  15928