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  2907  euind  2924  reuind  2942  eldifd  3139  eqssd  3172  ssrabdv  3234  elind  3320  dcun  3533  opm  4234  issod  4319  ordsucim  4499  onintonm  4516  ordtri2or2exmidlem  4525  en2lp  4553  ordwe  4575  sosng  4699  sotri2  5026  sotri3  5027  relssdmrn  5149  funun  5260  fnsng  5263  fnprg  5271  fntpg  5272  fntp  5273  fununi  5284  imain  5298  fnco  5324  f00  5407  f1ss  5427  f1ssr  5428  f1ssres  5430  f1f1orn  5472  foimacnv  5479  foun  5480  fun11iun  5482  sefvex  5536  dff3im  5661  fmpt  5666  ffnfv  5674  fmpt2d  5678  ffvresb  5679  fprg  5699  foco2  5754  fcof1  5783  fcofo  5784  fcof1o  5789  fliftf  5799  isoini2  5819  f1oiso  5826  moriotass  5858  fnoprabg  5975  f1ocnvd  6072  suppssfv  6078  suppssov1  6079  1stcof  6163  2ndcof  6164  1stconst  6221  2ndconst  6222  fo2ndf  6227  f1o2ndf1  6228  f1od2  6235  smores2  6294  tfrlem5  6314  tfrlemibfn  6328  tfr1onlembfn  6344  tfri1dALT  6351  tfrcllembfn  6357  nntri2  6494  eroveu  6625  elixpsn  6734  dom2lem  6771  xpf1o  6843  fidifsnen  6869  finexdc  6901  unfidisj  6920  f1finf1o  6945  fidcenumlemrks  6951  sbthlemi9  6963  supeuti  6992  infeuti  7027  casef1  7088  caseinl  7089  caseinr  7090  difinfsnlem  7097  ctmlemr  7106  ctm  7107  ctssdclemn0  7108  ctssdccl  7109  ctssdc  7111  enumctlemm  7112  nnnninf  7123  nninfwlpoimlemg  7172  en2other2  7194  exmidfodomrlemim  7199  pw1nel3  7229  dftap2  7249  cc2lem  7264  cc4f  7267  addclpi  7325  mulclpi  7326  nnppipi  7341  recmulnqg  7389  enq0ref  7431  nqnq0pi  7436  genipv  7507  addclpr  7535  nqprxx  7544  prmuloc  7564  mulclpr  7570  distrlem1prl  7580  distrlem1pru  7581  ltexprlempr  7606  ltexprlemrl  7608  ltexprlemru  7610  lteupri  7615  recexprlempr  7630  cauappcvgprlemm  7643  cauappcvgprlemopl  7644  cauappcvgprlemlol  7645  cauappcvgprlemopu  7646  cauappcvgprlemupu  7647  cauappcvgprlemloc  7650  cauappcvgprlemcl  7651  cauappcvgprlemladdfu  7652  cauappcvgprlemladdfl  7653  cauappcvgprlem2  7658  caucvgprlemm  7666  caucvgprlemopl  7667  caucvgprlemlol  7668  caucvgprlemopu  7669  caucvgprlemupu  7670  caucvgprlemloc  7673  caucvgprlemcl  7674  caucvgprlemladdfu  7675  caucvgprlem2  7678  caucvgprprlemml  7692  caucvgprprlemmu  7693  caucvgprprlemopl  7695  caucvgprprlemlol  7696  caucvgprprlemopu  7697  caucvgprprlemupu  7698  caucvgprprlemloc  7701  caucvgprprlemcl  7702  caucvgprprlem2  7708  suplocexprlemex  7720  suplocsrlem  7806  elrealeu  7827  rereceu  7887  axpre-suploclemres  7899  negf1o  8338  aptap  8606  receuap  8625  divvalap  8630  cju  8917  nn0ge2m1nn  9235  nnnegz  9255  elnnz  9262  elnn0z  9265  peano2z  9288  nn0n0n1ge2  9322  msqznn  9352  eluzaddi  9553  eluzsubi  9554  uzind4  9587  supinfneg  9594  infsupneg  9595  elnn1uz2  9606  uz2mulcl  9607  divfnzn  9620  nnrp  9662  rpaddcl  9676  rpmulcl  9677  rpdivcl  9678  rpgecl  9681  ge0p1rp  9684  elrpd  9692  ge0addcl  9980  ge0mulcl  9981  ge0xaddcl  9982  icoshftf1o  9990  peano2fzr  10036  uzsubsubfz  10046  fzsplit2  10049  elfznn  10053  fzss1  10062  fzss2  10063  fzp1elp1  10074  elfz1b  10089  elfz0fzfz0  10125  fz0fzelfz0  10126  difelfznle  10134  elfzofz  10161  fzosplitsnm1  10208  ubmelm1fzo  10225  fzofzp1b  10227  fzosplitsn  10232  exbtwnz  10250  flqge0nn0  10292  flqge1nn  10293  zmodcl  10343  modqmuladdnn0  10367  modsumfzodifsn  10395  frec2uzf1od  10405  frec2uzisod  10406  frecuzrdgrrn  10407  frec2uzrdg  10408  frecuzrdgrcl  10409  frecuzrdgtcl  10411  frecuzrdgsuc  10413  frecuzrdgrclt  10414  frecuzrdgfunlem  10418  frecuzrdgtclt  10420  frecuzrdgsuctlem  10422  uzennn  10435  seq3fveq2  10468  monoord  10475  iseqf1olemqcl  10485  iseqf1olemnab  10487  iseqf1olemab  10488  iseqf1olemqf1o  10492  seq3f1olemqsumkj  10497  seq3f1olemqsumk  10498  seq3id2  10508  exp3val  10521  expcl2lemap  10531  expclzaplem  10543  expge0  10555  expge1  10556  zsqcl2  10597  bcval4  10731  bcn1  10737  bccl2  10747  hashennnuni  10758  hashunlem  10783  hashdifpr  10799  zfz1isolem1  10819  seq3coll  10821  shftfn  10832  shftf  10838  recvguniq  11003  resqrexlemdecn  11020  rersqreu  11036  nn0abscl  11093  nnabscl  11108  abs2dif  11114  climuni  11300  2clim  11308  climcn2  11316  summodclem2a  11388  fsum3  11394  fsum3cvg3  11403  fsumcl2lem  11405  fsumadd  11413  fisum0diag2  11454  fsummulc2  11455  fsumge0  11466  geolim2  11519  cvgratnnlemabsle  11534  cvgratz  11539  mertenslemi1  11542  prodmodclem3  11582  prodmodclem2a  11583  fprodeq0  11624  fprodge0  11644  eff2  11687  tanvalap  11715  zdvdsdc  11818  fzo0dvdseq  11862  oexpneg  11881  oddge22np1  11885  evennn02n  11886  evennn2n  11887  nno  11910  divalglemeunn  11925  divalglemex  11926  divalglemeuneg  11927  divalg  11928  zsupcllemstep  11945  zsupcl  11947  divgcdz  11971  bezoutlemmain  11998  bezoutlemmo  12006  bezoutlemeu  12007  bezoutlemle  12008  sqgcd  12029  uzwodc  12037  eucalgval2  12052  eucalglt  12056  lcmcllem  12066  lcmledvds  12069  lcmneg  12073  lcmgcdlem  12076  ncoprmgcdne1b  12088  prmind2  12119  prmdc  12129  sqnprm  12135  isprm5lem  12140  isprm5  12141  isprm6  12146  sqrt2irrlem  12160  pw2dvdseu  12167  sqpweven  12174  2sqpwodd  12175  sqrt2irrap  12179  qgt0numnn  12198  phicl2  12213  hashdvds  12220  crth  12223  phimullem  12224  eulerthlem1  12226  eulerthlemh  12230  eulerthlemth  12231  hashgcdlem  12237  oddprm  12258  pythagtriplem6  12269  pythagtriplem11  12273  pythagtriplem13  12275  pythagtriplem19  12281  pclem0  12285  pcpremul  12292  pceu  12294  pc2dvds  12328  difsqpwdvds  12336  pcadd  12338  pockthlem  12353  pockthg  12354  1arith  12364  oddennn  12392  evenennn  12393  ennnfoneleminc  12411  ennnfonelemf1  12418  ennnfonelemen  12421  exmidunben  12426  ctinf  12430  ctiunctlemfo  12439  nninfdclemlt  12451  nninfdclemf1  12452  ptex  12712  imasaddfnlemg  12734  imasaddflemg  12736  mgmsscl  12779  sgrp0  12814  sgrp1  12815  hashfinmndnn  12832  ismndd  12837  mndpfo  12838  mhmf1o  12860  0mhm  12872  mhmco  12873  isgrpd2e  12895  grpinvf1o  12939  grpinvnzcl  12941  dfgrp3m  12968  mhmmnd  12979  ghmgrp  12981  mulgval  12985  mulgfng  12986  subgmulg  13046  issubg4m  13051  isnsg3  13065  nmzsubg  13068  ssnmz  13069  0nsg  13072  nsgid  13073  isabld  13100  srgfcl  13154  srglmhm  13174  srgrmhm  13175  iscrngd  13219  ringsrg  13222  unitabl  13284  ringelnzr  13326  subrgcrng  13344  subrgnzr  13361  tgtopon  13536  distopon  13557  epttop  13560  resttopon  13641  resttopon2  13648  cnco  13691  lmss  13716  txtopon  13732  uptx  13744  txdis1cn  13748  hmeocnv  13777  hmeof1o2  13778  hmeores  13785  hmeoco  13786  idhmeo  13787  txhmeo  13789  txswaphmeo  13791  psmetxrge0  13802  isxmet2d  13818  metres2  13851  xmetresbl  13910  comet  13969  bdxmet  13971  bdmet  13972  tgioo  14016  mulc1cncf  14046  mulcncflem  14060  cnrehmeocntop  14063  cnopnap  14064  dedekindeu  14071  dedekindicclemicc  14080  ivthinclemlm  14082  ivthinclemum  14083  ivthinclemlopn  14084  ivthinclemlr  14085  ivthinclemuopn  14086  ivthinclemur  14087  ivthinclemloc  14089  ivthinc  14091  dvfgg  14127  dvcjbr  14142  dvcj  14143  dvfre  14144  rplogbval  14333  lgsfcl2  14377  lgsval2lem  14381  lgsmod  14397  lgsdirprm  14405  lgsne0  14409  lgseisenlem1  14420  lgseisenlem2  14421  2sqlem8  14440  2sqlem9  14441  bj-charfundcALT  14531  bj-nnord  14680  bj-inf2vnlem1  14692  pwf1oexmid  14719  nnsf  14724  nninfall  14728  nninfself  14732  exmidsbthrlem  14740  qdencn  14745