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  2973  euind  2990  reuind  3008  eldifd  3207  eqssd  3241  ssrabdv  3303  elind  3389  dcun  3601  opm  4320  issod  4410  ordsucim  4592  onintonm  4609  ordtri2or2exmidlem  4618  en2lp  4646  ordwe  4668  sosng  4792  sotri2  5126  sotri3  5127  relssdmrn  5249  funun  5362  fnsng  5368  fnprg  5376  fntpg  5377  fntp  5378  fununi  5389  imain  5403  fnco  5431  f00  5519  f1ss  5539  f1ssr  5540  f1ssres  5542  f1f1orn  5585  foimacnv  5592  foun  5593  fun11iun  5595  sefvex  5650  dff3im  5782  fmpt  5787  ffnfv  5795  fmpt2d  5799  ffvresb  5800  fprg  5826  foco2  5883  fcof1  5913  fcofo  5914  fcof1o  5919  fliftf  5929  isoini2  5949  f1oiso  5956  moriotass  5991  fnoprabg  6111  f1ocnvd  6214  suppssfv  6220  suppssov1  6221  1stcof  6315  2ndcof  6316  1stconst  6373  2ndconst  6374  fo2ndf  6379  f1o2ndf1  6380  f1od2  6387  smores2  6446  tfrlem5  6466  tfrlemibfn  6480  tfr1onlembfn  6496  tfri1dALT  6503  tfrcllembfn  6509  nntri2  6648  eroveu  6781  elixpsn  6890  dom2lem  6931  xpf1o  7013  fidifsnen  7040  finexdc  7073  elssdc  7075  unfidisj  7095  f1finf1o  7125  fidcenumlemrks  7131  sbthlemi9  7143  supeuti  7172  infeuti  7207  casef1  7268  caseinl  7269  caseinr  7270  difinfsnlem  7277  ctmlemr  7286  ctm  7287  ctssdclemn0  7288  ctssdccl  7289  ctssdc  7291  enumctlemm  7292  nnnninf  7304  nninfwlpoimlemg  7353  en2other2  7385  exmidfodomrlemim  7390  pw1if  7421  pw1nel3  7427  dftap2  7448  cc2lem  7463  cc4f  7466  addclpi  7525  mulclpi  7526  nnppipi  7541  recmulnqg  7589  enq0ref  7631  nqnq0pi  7636  genipv  7707  addclpr  7735  nqprxx  7744  prmuloc  7764  mulclpr  7770  distrlem1prl  7780  distrlem1pru  7781  ltexprlempr  7806  ltexprlemrl  7808  ltexprlemru  7810  lteupri  7815  recexprlempr  7830  cauappcvgprlemm  7843  cauappcvgprlemopl  7844  cauappcvgprlemlol  7845  cauappcvgprlemopu  7846  cauappcvgprlemupu  7847  cauappcvgprlemloc  7850  cauappcvgprlemcl  7851  cauappcvgprlemladdfu  7852  cauappcvgprlemladdfl  7853  cauappcvgprlem2  7858  caucvgprlemm  7866  caucvgprlemopl  7867  caucvgprlemlol  7868  caucvgprlemopu  7869  caucvgprlemupu  7870  caucvgprlemloc  7873  caucvgprlemcl  7874  caucvgprlemladdfu  7875  caucvgprlem2  7878  caucvgprprlemml  7892  caucvgprprlemmu  7893  caucvgprprlemopl  7895  caucvgprprlemlol  7896  caucvgprprlemopu  7897  caucvgprprlemupu  7898  caucvgprprlemloc  7901  caucvgprprlemcl  7902  caucvgprprlem2  7908  suplocexprlemex  7920  suplocsrlem  8006  elrealeu  8027  rereceu  8087  axpre-suploclemres  8099  negf1o  8539  aptap  8808  receuap  8827  divvalap  8832  cju  9119  nn0ge2m1nn  9440  nnnegz  9460  elnnz  9467  elnn0z  9470  peano2z  9493  nn0n0n1ge2  9528  msqznn  9558  eluzaddi  9761  eluzsubi  9762  uzind4  9795  supinfneg  9802  infsupneg  9803  elnn1uz2  9814  uz2mulcl  9815  divfnzn  9828  nnrp  9871  rpaddcl  9885  rpmulcl  9886  rpdivcl  9887  rpgecl  9890  ge0p1rp  9893  elrpd  9901  ge0addcl  10189  ge0mulcl  10190  ge0xaddcl  10191  icoshftf1o  10199  peano2fzr  10245  uzsubsubfz  10255  fzsplit2  10258  elfznn  10262  fzss1  10271  fzss2  10272  fzp1elp1  10283  elfz1b  10298  elfz0fzfz0  10334  fz0fzelfz0  10335  difelfznle  10343  elfzofz  10371  fzosplitsnm1  10427  ubmelm1fzo  10444  fzofzp1b  10446  fzosplitsn  10451  zsupcllemstep  10461  zsupcl  10463  exbtwnz  10482  flqge0nn0  10525  flqge1nn  10526  zmodcl  10578  modqmuladdnn0  10602  modsumfzodifsn  10630  frec2uzf1od  10640  frec2uzisod  10641  frecuzrdgrrn  10642  frec2uzrdg  10643  frecuzrdgrcl  10644  frecuzrdgtcl  10646  frecuzrdgsuc  10648  frecuzrdgrclt  10649  frecuzrdgfunlem  10653  frecuzrdgtclt  10655  frecuzrdgsuctlem  10657  uzennn  10670  seq3fveq2  10709  seqfveq2g  10711  monoord  10719  iseqf1olemqcl  10733  iseqf1olemnab  10735  iseqf1olemab  10736  iseqf1olemqf1o  10740  seq3f1olemqsumkj  10745  seq3f1olemqsumk  10746  seq3id2  10760  exp3val  10775  expcl2lemap  10785  expclzaplem  10797  expge0  10809  expge1  10810  zsqcl2  10851  bcval4  10986  bcn1  10992  bccl2  11002  hashennnuni  11013  hashunlem  11038  hashdifpr  11055  zfz1isolem1  11075  seq3coll  11077  iswrdiz  11091  ccatsymb  11150  ccatrn  11157  swrds1  11215  swrdccat2  11218  swrdccatin2  11276  pfxccatin12lem2  11278  pfxccatin12lem3  11279  pfxccatin12  11280  pfxccat3  11281  pfxccat3a  11285  shftfn  11350  shftf  11356  recvguniq  11521  resqrexlemdecn  11538  rersqreu  11554  nn0abscl  11611  nnabscl  11626  abs2dif  11632  nn0maxcl  11751  climuni  11819  2clim  11827  climcn2  11835  summodclem2a  11907  fsum3  11913  fsum3cvg3  11922  fsumcl2lem  11924  fsumadd  11932  fisum0diag2  11973  fsummulc2  11974  fsumge0  11985  geolim2  12038  cvgratnnlemabsle  12053  cvgratz  12058  mertenslemi1  12061  prodmodclem3  12101  prodmodclem2a  12102  fprodeq0  12143  fprodge0  12163  eff2  12206  tanvalap  12234  zdvdsdc  12338  fzo0dvdseq  12383  oexpneg  12403  oddge22np1  12407  evennn02n  12408  evennn2n  12409  nno  12432  divalglemeunn  12447  divalglemex  12448  divalglemeuneg  12449  divalg  12450  bitsfzolem  12480  bitsinv1lem  12487  divgcdz  12507  bezoutlemmain  12534  bezoutlemmo  12542  bezoutlemeu  12543  bezoutlemle  12544  sqgcd  12565  uzwodc  12573  nninfctlemfo  12576  eucalgval2  12590  eucalglt  12594  lcmneg  12611  lcmgcdlem  12614  ncoprmgcdne1b  12626  prmind2  12657  prmdc  12667  sqnprm  12673  isprm5lem  12678  isprm5  12679  isprm6  12684  sqrt2irrlem  12698  pw2dvdseu  12705  sqpweven  12712  2sqpwodd  12713  sqrt2irrap  12717  qgt0numnn  12736  phicl2  12751  hashdvds  12758  crth  12761  phimullem  12762  eulerthlem1  12764  eulerthlemh  12768  eulerthlemth  12769  hashgcdlem  12775  oddprm  12797  pythagtriplem6  12808  pythagtriplem11  12812  pythagtriplem13  12814  pythagtriplem19  12820  pclem0  12824  pcpremul  12831  pceu  12833  pc2dvds  12868  difsqpwdvds  12876  pcadd  12878  pockthlem  12894  pockthg  12895  1arith  12905  4sqlemffi  12934  4sqlem11  12939  4sqlem12  12940  4sqlem13m  12941  4sqlem14  12942  4sqlem17  12945  oddennn  12978  evenennn  12979  ennnfoneleminc  12997  ennnfonelemf1  13004  ennnfonelemen  13007  exmidunben  13012  ctinf  13016  ctiunctlemfo  13025  nninfdclemlt  13037  nninfdclemf1  13038  ptex  13312  imasaddfnlemg  13362  imasaddflemg  13364  mgmsscl  13409  sgrp0  13458  sgrp1  13459  hashfinmndnn  13480  ismndd  13485  mndpfo  13486  mhmf1o  13518  0mhm  13534  resmhm  13535  resmhm2  13536  resmhm2b  13537  mhmco  13538  gsumvallem2  13541  isgrpd2e  13568  grpinvf1o  13618  grpinvnzcl  13620  dfgrp3m  13647  mhmmnd  13668  ghmgrp  13670  mulgval  13674  mulgfng  13676  subgmulg  13740  issubg4m  13745  isnsg3  13759  nmzsubg  13762  ssnmz  13763  0nsg  13766  nsgid  13767  ghmnsgima  13820  ghmnsgpreima  13821  ghmf1  13825  kerf1ghm  13826  ghmf1o  13827  conjnmzb  13832  isabld  13851  ghmcmn  13879  ghmabl  13880  invghm  13881  srgfcl  13951  srglmhm  13971  srgrmhm  13972  iscrngd  14020  ringsrg  14025  unitabl  14096  rhmf1o  14147  rhmco  14153  ringelnzr  14166  subrngringnsg  14184  subrgcrng  14204  subrgnzr  14221  resrhm  14227  unitrrg  14246  lssneln0  14353  rnglidlmsgrp  14476  quscrng  14512  expghmap  14586  mulgghm2  14587  znf1o  14630  znidom  14636  znidomb  14637  psrbaglesuppg  14651  tgtopon  14755  distopon  14776  epttop  14779  resttopon  14860  resttopon2  14867  cnco  14910  lmss  14935  txtopon  14951  uptx  14963  txdis1cn  14967  hmeocnv  14996  hmeof1o2  14997  hmeores  15004  hmeoco  15005  idhmeo  15006  txhmeo  15008  txswaphmeo  15010  psmetxrge0  15021  isxmet2d  15037  metres2  15070  xmetresbl  15129  comet  15188  bdxmet  15190  bdmet  15191  tgioo  15243  mulc1cncf  15278  mulcncflem  15296  cnrehmeocntop  15299  cnopnap  15300  dedekindeu  15312  dedekindicclemicc  15321  ivthinclemlm  15323  ivthinclemum  15324  ivthinclemlopn  15325  ivthinclemlr  15326  ivthinclemuopn  15327  ivthinclemur  15328  ivthinclemloc  15330  ivthinc  15332  ivthreinc  15334  dvfgg  15377  dvcjbr  15397  dvcj  15398  dvfre  15399  elplyr  15429  plyreres  15453  rplogbval  15634  sgmnncl  15677  mpodvdsmulf1o  15679  mersenne  15686  perfectlem2  15689  lgsfcl2  15700  lgsval2lem  15704  lgsmod  15720  lgsdirprm  15728  lgsne0  15732  gausslemma2dlem0h  15750  gausslemma2dlem1a  15752  gausslemma2dlem1f1o  15754  gausslemma2dlem4  15758  lgseisenlem1  15764  lgseisenlem2  15765  lgsquadlem1  15771  lgsquadlem2  15772  lgsquad2lem2  15776  2sqlem8  15817  2sqlem9  15818  structiedg0val  15856  ausgrumgrien  15983  usgredgreu  16029  uspgredg2vtxeu  16031  uspgredg2v  16034  usgredg2v  16037  trlres  16128  clwwlkbp  16133  clwwlkccatlem  16137  bj-charfundcALT  16227  bj-nnord  16376  bj-inf2vnlem1  16388  pwf1oexmid  16424  nnsf  16431  nninfall  16435  nninfself  16439  exmidsbthrlem  16450  qdencn  16455