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  941  ecase2d  1388  sb2  1815  sbequ1  1816  sbidm  1899  eqeu  2977  euind  2994  reuind  3012  eldifd  3211  eqssd  3245  ssrabdv  3307  elind  3394  dcun  3606  opm  4332  issod  4422  ordsucim  4604  onintonm  4621  ordtri2or2exmidlem  4630  en2lp  4658  ordwe  4680  sosng  4805  sotri2  5141  sotri3  5142  relssdmrn  5264  funun  5378  fnsng  5384  fnprg  5392  fntpg  5393  fntp  5394  fununi  5405  imain  5419  fnco  5447  f00  5537  f1ss  5557  f1ssr  5558  f1ssres  5560  f1f1orn  5603  foimacnv  5610  foun  5611  fun11iun  5613  sefvex  5669  dff3im  5800  fmpt  5805  ffnfv  5813  fmpt2d  5817  ffvresb  5818  fprg  5845  foco2  5904  fcof1  5934  fcofo  5935  fcof1o  5940  fliftf  5950  isoini2  5970  f1oiso  5977  moriotass  6012  fnoprabg  6132  f1ocnvd  6235  suppssov1  6241  1stcof  6335  2ndcof  6336  1stconst  6395  2ndconst  6396  fo2ndf  6401  f1o2ndf1  6402  f1od2  6409  suppssfvg  6441  smores2  6503  tfrlem5  6523  tfrlemibfn  6537  tfr1onlembfn  6553  tfri1dALT  6560  tfrcllembfn  6566  nntri2  6705  eroveu  6838  elixpsn  6947  dom2lem  6988  xpf1o  7073  fidifsnen  7100  finexdc  7135  elssdc  7137  unfidisj  7157  f1finf1o  7189  fidcenumlemrks  7195  sbthlemi9  7207  supeuti  7236  infeuti  7271  casef1  7332  caseinl  7333  caseinr  7334  difinfsnlem  7341  ctmlemr  7350  ctm  7351  ctssdclemn0  7352  ctssdccl  7353  ctssdc  7355  enumctlemm  7356  nnnninf  7368  nninfwlpoimlemg  7417  en2other2  7450  exmidfodomrlemim  7455  pw1if  7486  pw1nel3  7492  dftap2  7513  cc2lem  7528  cc4f  7531  addclpi  7590  mulclpi  7591  nnppipi  7606  recmulnqg  7654  enq0ref  7696  nqnq0pi  7701  genipv  7772  addclpr  7800  nqprxx  7809  prmuloc  7829  mulclpr  7835  distrlem1prl  7845  distrlem1pru  7846  ltexprlempr  7871  ltexprlemrl  7873  ltexprlemru  7875  lteupri  7880  recexprlempr  7895  cauappcvgprlemm  7908  cauappcvgprlemopl  7909  cauappcvgprlemlol  7910  cauappcvgprlemopu  7911  cauappcvgprlemupu  7912  cauappcvgprlemloc  7915  cauappcvgprlemcl  7916  cauappcvgprlemladdfu  7917  cauappcvgprlemladdfl  7918  cauappcvgprlem2  7923  caucvgprlemm  7931  caucvgprlemopl  7932  caucvgprlemlol  7933  caucvgprlemopu  7934  caucvgprlemupu  7935  caucvgprlemloc  7938  caucvgprlemcl  7939  caucvgprlemladdfu  7940  caucvgprlem2  7943  caucvgprprlemml  7957  caucvgprprlemmu  7958  caucvgprprlemopl  7960  caucvgprprlemlol  7961  caucvgprprlemopu  7962  caucvgprprlemupu  7963  caucvgprprlemloc  7966  caucvgprprlemcl  7967  caucvgprprlem2  7973  suplocexprlemex  7985  suplocsrlem  8071  elrealeu  8092  rereceu  8152  axpre-suploclemres  8164  negf1o  8603  aptap  8872  receuap  8891  divvalap  8896  cju  9183  nn0ge2m1nn  9506  nnnegz  9526  elnnz  9533  elnn0z  9536  peano2z  9559  nn0n0n1ge2  9594  msqznn  9624  eluzaddi  9827  eluzsubi  9828  uzind4  9866  supinfneg  9873  infsupneg  9874  elnn1uz2  9885  uz2mulcl  9886  divfnzn  9899  nnrp  9942  rpaddcl  9956  rpmulcl  9957  rpdivcl  9958  rpgecl  9961  ge0p1rp  9964  elrpd  9972  ge0addcl  10260  ge0mulcl  10261  ge0xaddcl  10262  icoshftf1o  10270  peano2fzr  10317  uzsubsubfz  10327  fzsplit2  10330  elfznn  10334  fzss1  10343  fzss2  10344  fzp1elp1  10355  elfz1b  10370  elfz0fzfz0  10406  fz0fzelfz0  10407  difelfznle  10415  elfzofz  10443  nn0p1elfzo  10467  fzosplitsnm1  10500  ubmelm1fzo  10517  fzofzp1b  10519  fzosplitsn  10524  zsupcllemstep  10535  zsupcl  10537  exbtwnz  10556  flqge0nn0  10599  flqge1nn  10600  zmodcl  10652  modqmuladdnn0  10676  modsumfzodifsn  10704  frec2uzf1od  10714  frec2uzisod  10715  frecuzrdgrrn  10716  frec2uzrdg  10717  frecuzrdgrcl  10718  frecuzrdgtcl  10720  frecuzrdgsuc  10722  frecuzrdgrclt  10723  frecuzrdgfunlem  10727  frecuzrdgtclt  10729  frecuzrdgsuctlem  10731  uzennn  10744  seq3fveq2  10783  seqfveq2g  10785  monoord  10793  iseqf1olemqcl  10807  iseqf1olemnab  10809  iseqf1olemab  10810  iseqf1olemqf1o  10814  seq3f1olemqsumkj  10819  seq3f1olemqsumk  10820  seq3id2  10834  exp3val  10849  expcl2lemap  10859  expclzaplem  10871  expge0  10883  expge1  10884  zsqcl2  10925  bcval4  11060  bcn1  11066  bccl2  11076  hashennnuni  11087  hashunlem  11113  hashdifpr  11130  zfz1isolem1  11150  seq3coll  11152  iswrdiz  11169  ccatsymb  11228  ccatrn  11235  ccat2s1fvwd  11273  swrds1  11298  swrdccat2  11301  swrdccatin2  11359  pfxccatin12lem2  11361  pfxccatin12lem3  11362  pfxccatin12  11363  pfxccat3  11364  pfxccat3a  11368  shftfn  11447  shftf  11453  recvguniq  11618  resqrexlemdecn  11635  rersqreu  11651  nn0abscl  11708  nnabscl  11723  abs2dif  11729  nn0maxcl  11848  climuni  11916  2clim  11924  climcn2  11932  summodclem2a  12005  fsum3  12011  fsum3cvg3  12020  fsumcl2lem  12022  fsumadd  12030  fisum0diag2  12071  fsummulc2  12072  fsumge0  12083  geolim2  12136  cvgratnnlemabsle  12151  cvgratz  12156  mertenslemi1  12159  prodmodclem3  12199  prodmodclem2a  12200  fprodeq0  12241  fprodge0  12261  eff2  12304  tanvalap  12332  zdvdsdc  12436  fzo0dvdseq  12481  oexpneg  12501  oddge22np1  12505  evennn02n  12506  evennn2n  12507  nno  12530  divalglemeunn  12545  divalglemex  12546  divalglemeuneg  12547  divalg  12548  bitsfzolem  12578  bitsinv1lem  12585  divgcdz  12605  bezoutlemmain  12632  bezoutlemmo  12640  bezoutlemeu  12641  bezoutlemle  12642  sqgcd  12663  uzwodc  12671  nninfctlemfo  12674  eucalgval2  12688  eucalglt  12692  lcmneg  12709  lcmgcdlem  12712  ncoprmgcdne1b  12724  prmind2  12755  prmdc  12765  sqnprm  12771  isprm5lem  12776  isprm5  12777  isprm6  12782  sqrt2irrlem  12796  pw2dvdseu  12803  sqpweven  12810  2sqpwodd  12811  sqrt2irrap  12815  qgt0numnn  12834  phicl2  12849  hashdvds  12856  crth  12859  phimullem  12860  eulerthlem1  12862  eulerthlemh  12866  eulerthlemth  12867  hashgcdlem  12873  oddprm  12895  pythagtriplem6  12906  pythagtriplem11  12910  pythagtriplem13  12912  pythagtriplem19  12918  pclem0  12922  pcpremul  12929  pceu  12931  pc2dvds  12966  difsqpwdvds  12974  pcadd  12976  pockthlem  12992  pockthg  12993  1arith  13003  4sqlemffi  13032  4sqlem11  13037  4sqlem12  13038  4sqlem13m  13039  4sqlem14  13040  4sqlem17  13043  oddennn  13076  evenennn  13077  ennnfoneleminc  13095  ennnfonelemf1  13102  ennnfonelemen  13105  exmidunben  13110  ctinf  13114  ctiunctlemfo  13123  nninfdclemlt  13135  nninfdclemf1  13136  ptex  13410  imasaddfnlemg  13460  imasaddflemg  13462  mgmsscl  13507  sgrp0  13556  sgrp1  13557  hashfinmndnn  13578  ismndd  13583  mndpfo  13584  mhmf1o  13616  0mhm  13632  resmhm  13633  resmhm2  13634  resmhm2b  13635  mhmco  13636  gsumvallem2  13639  isgrpd2e  13666  grpinvf1o  13716  grpinvnzcl  13718  dfgrp3m  13745  mhmmnd  13766  ghmgrp  13768  mulgval  13772  mulgfng  13774  subgmulg  13838  issubg4m  13843  isnsg3  13857  nmzsubg  13860  ssnmz  13861  0nsg  13864  nsgid  13865  ghmnsgima  13918  ghmnsgpreima  13919  ghmf1  13923  kerf1ghm  13924  ghmf1o  13925  conjnmzb  13930  isabld  13949  ghmcmn  13977  ghmabl  13978  invghm  13979  srgfcl  14050  srglmhm  14070  srgrmhm  14071  iscrngd  14119  ringsrg  14124  unitabl  14195  rhmf1o  14246  rhmco  14252  ringelnzr  14265  subrngringnsg  14283  subrgcrng  14303  subrgnzr  14320  resrhm  14326  unitrrg  14346  lssneln0  14453  rnglidlmsgrp  14576  quscrng  14612  expghmap  14686  mulgghm2  14687  znf1o  14730  znidom  14736  znidomb  14737  psrbaglesuppg  14751  psrbagcon  14755  tgtopon  14860  distopon  14881  epttop  14884  resttopon  14965  resttopon2  14972  cnco  15015  lmss  15040  txtopon  15056  uptx  15068  txdis1cn  15072  hmeocnv  15101  hmeof1o2  15102  hmeores  15109  hmeoco  15110  idhmeo  15111  txhmeo  15113  txswaphmeo  15115  psmetxrge0  15126  isxmet2d  15142  metres2  15175  xmetresbl  15234  comet  15293  bdxmet  15295  bdmet  15296  tgioo  15348  mulc1cncf  15383  mulcncflem  15401  cnrehmeocntop  15404  cnopnap  15405  dedekindeu  15417  dedekindicclemicc  15426  ivthinclemlm  15428  ivthinclemum  15429  ivthinclemlopn  15430  ivthinclemlr  15431  ivthinclemuopn  15432  ivthinclemur  15433  ivthinclemloc  15435  ivthinc  15437  ivthreinc  15439  dvfgg  15482  dvcjbr  15502  dvcj  15503  dvfre  15504  elplyr  15534  plyreres  15558  rplogbval  15739  sgmnncl  15785  mpodvdsmulf1o  15787  mersenne  15794  perfectlem2  15797  lgsfcl2  15808  lgsval2lem  15812  lgsmod  15828  lgsdirprm  15836  lgsne0  15840  gausslemma2dlem0h  15858  gausslemma2dlem1a  15860  gausslemma2dlem1f1o  15862  gausslemma2dlem4  15866  lgseisenlem1  15872  lgseisenlem2  15873  lgsquadlem1  15879  lgsquadlem2  15880  lgsquad2lem2  15884  2sqlem8  15925  2sqlem9  15926  structiedg0val  15964  ausgrumgrien  16094  usgredgreu  16140  uspgredg2vtxeu  16142  uspgredg2v  16145  usgredg2v  16148  usgr1e  16165  subuhgr  16196  subupgr  16197  subumgr  16198  subusgr  16199  vdegp1aid  16238  trlres  16314  clwwlkbp  16319  clwwlkccatlem  16324  s2elclwwlknon2  16360  clwwlknonex2lem2  16362  clwwlknonex2e  16364  bj-charfundcALT  16508  bj-nnord  16657  bj-inf2vnlem1  16669  pwf1oexmid  16704  nnsf  16714  nninfall  16718  nninfself  16722  exmidsbthrlem  16733  qdencn  16738  gfsumval  16792