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  1816  sbequ1  1817  sbidm  1900  eqeu  2987  euind  3004  reuind  3022  eldifd  3221  eqssd  3255  ssrabdv  3317  elind  3404  dcun  3619  opm  4350  issod  4440  ordsucim  4622  onintonm  4639  ordtri2or2exmidlem  4648  en2lp  4676  ordwe  4698  sosng  4823  sotri2  5160  sotri3  5161  relssdmrn  5283  funun  5397  fnsng  5403  fnprg  5411  fntpg  5412  fntp  5413  fununi  5424  imain  5438  fnco  5466  f00  5559  f1ss  5579  f1ssr  5580  f1ssres  5582  f1f1orn  5625  foimacnv  5632  foun  5633  fun11iun  5635  sefvex  5691  dff3im  5822  fmpt  5827  ffnfv  5835  fmpt2d  5839  ffvresb  5840  fprg  5867  foco2  5926  fcof1  5956  fcofo  5957  fcof1o  5962  fliftf  5972  isoini2  5992  f1oiso  5999  moriotass  6034  fnoprabg  6154  f1ocnvd  6257  suppssov1  6263  1stcof  6357  2ndcof  6358  1stconst  6417  2ndconst  6418  fo2ndf  6423  f1o2ndf1  6424  f1od2  6431  suppssfvg  6463  smores2  6525  tfrlem5  6545  tfrlemibfn  6559  tfr1onlembfn  6575  tfri1dALT  6582  tfrcllembfn  6588  nntri2  6727  eroveu  6860  elixpsn  6970  dom2lem  7011  xpf1o  7097  fidifsnen  7125  finexdc  7160  elssdc  7162  unfidisj  7182  f1finf1o  7217  fidcenumlemrks  7223  sbthlemi9  7235  supeuti  7285  infeuti  7320  casef1  7381  caseinl  7382  caseinr  7383  difinfsnlem  7390  ctmlemr  7399  ctm  7400  ctssdclemn0  7401  ctssdccl  7402  ctssdc  7404  enumctlemm  7405  nnnninf  7417  nninfwlpoimlemg  7466  en2other2  7499  exmidfodomrlemim  7504  pw1if  7535  pw1nel3  7541  dftap2  7565  cc2lem  7580  cc4f  7583  addclpi  7642  mulclpi  7643  nnppipi  7658  recmulnqg  7706  enq0ref  7748  nqnq0pi  7753  genipv  7824  addclpr  7852  nqprxx  7861  prmuloc  7881  mulclpr  7887  distrlem1prl  7897  distrlem1pru  7898  ltexprlempr  7923  ltexprlemrl  7925  ltexprlemru  7927  lteupri  7932  recexprlempr  7947  cauappcvgprlemm  7960  cauappcvgprlemopl  7961  cauappcvgprlemlol  7962  cauappcvgprlemopu  7963  cauappcvgprlemupu  7964  cauappcvgprlemloc  7967  cauappcvgprlemcl  7968  cauappcvgprlemladdfu  7969  cauappcvgprlemladdfl  7970  cauappcvgprlem2  7975  caucvgprlemm  7983  caucvgprlemopl  7984  caucvgprlemlol  7985  caucvgprlemopu  7986  caucvgprlemupu  7987  caucvgprlemloc  7990  caucvgprlemcl  7991  caucvgprlemladdfu  7992  caucvgprlem2  7995  caucvgprprlemml  8009  caucvgprprlemmu  8010  caucvgprprlemopl  8012  caucvgprprlemlol  8013  caucvgprprlemopu  8014  caucvgprprlemupu  8015  caucvgprprlemloc  8018  caucvgprprlemcl  8019  caucvgprprlem2  8025  suplocexprlemex  8037  suplocsrlem  8123  elrealeu  8144  rereceu  8204  axpre-suploclemres  8216  negf1o  8655  aptap  8924  receuap  8943  divvalap  8948  cju  9235  nn0ge2m1nn  9560  nnnegz  9580  elnnz  9587  elnn0z  9590  peano2z  9613  nn0n0n1ge2  9648  msqznn  9678  eluzaddi  9881  eluzsubi  9882  uzind4  9920  supinfneg  9927  infsupneg  9928  elnn1uz2  9939  uz2mulcl  9940  divfnzn  9953  nnrp  9996  rpaddcl  10010  rpmulcl  10011  rpdivcl  10012  rpgecl  10015  ge0p1rp  10018  elrpd  10026  ge0addcl  10314  ge0mulcl  10315  ge0xaddcl  10316  icoshftf1o  10324  peano2fzr  10371  uzsubsubfz  10381  fzsplit2  10384  elfznn  10388  fzss1  10397  fzss2  10398  fzp1elp1  10409  elfz1b  10424  elfz0fzfz0  10460  fz0fzelfz0  10461  difelfznle  10469  elfzofz  10497  nn0p1elfzo  10521  fzosplitsnm1  10554  ubmelm1fzo  10571  fzofzp1b  10573  fzosplitsn  10578  zsupcllemstep  10589  zsupcl  10591  exbtwnz  10610  flqge0nn0  10653  flqge1nn  10654  zmodcl  10706  modqmuladdnn0  10730  modsumfzodifsn  10758  frec2uzf1od  10768  frec2uzisod  10769  frecuzrdgrrn  10770  frec2uzrdg  10771  frecuzrdgrcl  10772  frecuzrdgtcl  10774  frecuzrdgsuc  10776  frecuzrdgrclt  10777  frecuzrdgfunlem  10781  frecuzrdgtclt  10783  frecuzrdgsuctlem  10785  uzennn  10798  seq3fveq2  10837  seqfveq2g  10839  monoord  10847  iseqf1olemqcl  10861  iseqf1olemnab  10863  iseqf1olemab  10864  iseqf1olemqf1o  10868  seq3f1olemqsumkj  10873  seq3f1olemqsumk  10874  seq3id2  10888  exp3val  10903  expcl2lemap  10913  expclzaplem  10925  expge0  10937  expge1  10938  zsqcl2  10979  bcval4  11114  bcn1  11120  bccl2  11130  hashennnuni  11142  hashunlem  11168  hashdifpr  11185  zfz1isolem1  11212  seq3coll  11214  iswrdiz  11231  ccatsymb  11290  ccatrn  11297  ccat2s1fvwd  11335  swrds1  11360  swrdccat2  11363  swrdccatin2  11421  pfxccatin12lem2  11423  pfxccatin12lem3  11424  pfxccatin12  11425  pfxccat3  11426  pfxccat3a  11430  shftfn  11509  shftf  11515  recvguniq  11680  resqrexlemdecn  11697  rersqreu  11713  nn0abscl  11770  nnabscl  11785  abs2dif  11791  nn0maxcl  11910  climuni  11978  2clim  11986  climcn2  11994  summodclem2a  12067  fsum3  12073  fsum3cvg3  12082  fsumcl2lem  12084  fsumadd  12092  fisum0diag2  12133  fsummulc2  12134  fsumge0  12145  geolim2  12198  cvgratnnlemabsle  12213  cvgratz  12218  mertenslemi1  12221  prodmodclem3  12261  prodmodclem2a  12262  fprodeq0  12303  fprodge0  12323  eff2  12366  tanvalap  12394  zdvdsdc  12498  fzo0dvdseq  12543  oexpneg  12563  oddge22np1  12567  evennn02n  12568  evennn2n  12569  nno  12592  divalglemeunn  12607  divalglemex  12608  divalglemeuneg  12609  divalg  12610  bitsfzolem  12640  bitsinv1lem  12647  divgcdz  12667  bezoutlemmain  12694  bezoutlemmo  12702  bezoutlemeu  12703  bezoutlemle  12704  sqgcd  12725  uzwodc  12733  nninfctlemfo  12736  eucalgval2  12750  eucalglt  12754  lcmneg  12771  lcmgcdlem  12774  ncoprmgcdne1b  12786  prmind2  12817  prmdc  12827  sqnprm  12833  isprm5lem  12838  isprm5  12839  isprm6  12844  sqrt2irrlem  12858  pw2dvdseu  12865  sqpweven  12872  2sqpwodd  12873  sqrt2irrap  12877  qgt0numnn  12896  phicl2  12911  crth  12921  phimullem  12922  eulerthlem1  12924  eulerthlemh  12928  eulerthlemth  12929  hashgcdlem  12935  oddprm  12957  pythagtriplem6  12968  pythagtriplem11  12972  pythagtriplem13  12974  pythagtriplem19  12980  pclem0  12984  pcpremul  12991  pceu  12993  pc2dvds  13028  difsqpwdvds  13036  pcadd  13038  pockthlem  13054  pockthg  13055  1arith  13065  4sqlemffi  13094  4sqlem11  13099  4sqlem12  13100  4sqlem13m  13101  4sqlem14  13102  4sqlem17  13105  oddennn  13143  evenennn  13144  ennnfoneleminc  13162  ennnfonelemf1  13169  ennnfonelemen  13172  exmidunben  13177  ctinf  13181  ctiunctlemfo  13190  nninfdclemlt  13202  nninfdclemf1  13203  ptex  13477  imasaddfnlemg  13527  imasaddflemg  13529  mgmsscl  13574  sgrp0  13623  sgrp1  13624  hashfinmndnn  13645  ismndd  13650  mndpfo  13651  mhmf1o  13683  0mhm  13699  resmhm  13700  resmhm2  13701  resmhm2b  13702  mhmco  13703  gsumvallem2  13706  isgrpd2e  13733  grpinvf1o  13783  grpinvnzcl  13785  dfgrp3m  13812  mhmmnd  13833  ghmgrp  13835  mulgval  13839  mulgfng  13841  subgmulg  13905  issubg4m  13910  isnsg3  13924  nmzsubg  13927  ssnmz  13928  0nsg  13931  nsgid  13932  ghmnsgima  13985  ghmnsgpreima  13986  ghmf1  13990  kerf1ghm  13991  ghmf1o  13992  conjnmzb  13997  isabld  14016  ghmcmn  14044  ghmabl  14045  invghm  14046  srgfcl  14117  srglmhm  14137  srgrmhm  14138  iscrngd  14186  ringsrg  14191  unitabl  14262  rhmf1o  14313  rhmco  14319  ringelnzr  14332  subrngringnsg  14350  subrgcrng  14370  subrgnzr  14387  resrhm  14393  unitrrg  14413  aprnzr  14433  aprlring  14434  lssneln0  14522  rnglidlmsgrp  14645  quscrng  14681  expghmap  14755  mulgghm2  14756  znf1o  14799  znidom  14805  znidomb  14806  psrbaglesuppg  14821  psrbagcon  14826  tgtopon  14931  distopon  14952  epttop  14955  resttopon  15036  resttopon2  15043  cnco  15086  lmss  15111  txtopon  15127  uptx  15139  txdis1cn  15143  hmeocnv  15172  hmeof1o2  15173  hmeores  15180  hmeoco  15181  idhmeo  15182  txhmeo  15184  txswaphmeo  15186  psmetxrge0  15197  isxmet2d  15213  metres2  15246  xmetresbl  15305  comet  15364  bdxmet  15366  bdmet  15367  tgioo  15419  mulc1cncf  15454  mulcncflem  15472  cnrehmeocntop  15475  cnopnap  15476  dedekindeu  15488  dedekindicclemicc  15497  ivthinclemlm  15499  ivthinclemum  15500  ivthinclemlopn  15501  ivthinclemlr  15502  ivthinclemuopn  15503  ivthinclemur  15504  ivthinclemloc  15506  ivthinc  15508  ivthreinc  15510  dvfgg  15553  dvcjbr  15573  dvcj  15574  dvfre  15575  elplyr  15605  plyreres  15629  rplogbval  15810  sgmnncl  15856  mpodvdsmulf1o  15858  mersenne  15865  perfectlem2  15868  lgsfcl2  15879  lgsval2lem  15883  lgsmod  15899  lgsdirprm  15907  lgsne0  15911  gausslemma2dlem0h  15929  gausslemma2dlem1a  15931  gausslemma2dlem1f1o  15933  gausslemma2dlem4  15937  lgseisenlem1  15943  lgseisenlem2  15944  lgsquadlem1  15950  lgsquadlem2  15951  lgsquad2lem2  15955  2sqlem8  15996  2sqlem9  15997  structiedg0val  16035  ausgrumgrien  16165  usgredgreu  16211  uspgredg2vtxeu  16213  uspgredg2v  16216  usgredg2v  16219  usgr1e  16236  subuhgr  16267  subupgr  16268  subumgr  16269  subusgr  16270  vdegp1aid  16309  trlres  16385  clwwlkbp  16390  clwwlkccatlem  16395  s2elclwwlknon2  16431  clwwlknonex2lem2  16433  clwwlknonex2e  16435  bj-charfundcALT  16579  bj-nnord  16728  bj-inf2vnlem1  16740  pwf1oexmid  16773  nnsf  16783  nninfall  16787  nninfself  16791  exmidsbthrlem  16802  qdencn  16807  gfsumval  16862