Theorem sylanbrc 421

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  945  ecase2d  1392  sb2  1820  sbequ1  1821  sbidm  1904  eqeu  2996  euind  3013  reuind  3031  eldifd  3230  eqssd  3265  ssrabdv  3327  elind  3414  dcun  3634  opm  4369  issod  4459  ordsucim  4642  onintonm  4659  ordtri2or2exmidlem  4668  en2lp  4696  ordwe  4718  sosng  4843  sotri2  5180  sotri3  5181  relssdmrn  5303  funun  5417  fnsng  5423  fnprg  5431  fntpg  5432  fntp  5433  fununi  5444  imain  5458  fnco  5486  f00  5579  f1ss  5599  f1ssr  5600  f1ssres  5602  f1f1orn  5645  foimacnv  5652  foun  5653  fun11iun  5655  sefvex  5711  dff3im  5844  fmpt  5849  ffnfv  5857  fmpt2d  5861  ffvresb  5862  fprg  5889  foco2  5949  fcof1  5979  fcofo  5980  fcof1o  5985  fliftf  5995  isoini2  6015  f1oiso  6022  moriotass  6059  fnoprabg  6179  f1ocnvd  6282  f1o3d  6288  suppssov1  6289  1stcof  6387  2ndcof  6388  1stconst  6447  2ndconst  6448  fo2ndf  6453  f1o2ndf1  6454  f1od2  6461  suppssfvg  6493  smores2  6555  tfrlem5  6575  tfrlemibfn  6589  tfr1onlembfn  6605  tfri1dALT  6612  tfrcllembfn  6618  nntri2  6757  eroveu  6890  elixpsn  7007  dom2lem  7048  xpf1o  7134  fidifsnen  7162  finexdc  7197  elssdc  7199  unfidisj  7219  f1finf1o  7254  fidcenumlemrks  7260  sbthlemi9  7272  supeuti  7324  infeuti  7359  casef1  7420  caseinl  7421  caseinr  7422  difinfsnlem  7429  ctmlemr  7438  ctm  7439  ctssdclemn0  7440  ctssdccl  7441  ctssdc  7443  enumctlemm  7444  nnnninf  7456  nninfwlpoimlemg  7505  en2other2  7538  exmidfodomrlemim  7543  pw1if  7574  pw1nel3  7580  dftap2  7607  cc2lem  7622  cc4f  7625  addclpi  7684  mulclpi  7685  nnppipi  7700  recmulnqg  7748  enq0ref  7790  nqnq0pi  7795  genipv  7866  addclpr  7894  nqprxx  7903  prmuloc  7923  mulclpr  7929  distrlem1prl  7939  distrlem1pru  7940  ltexprlempr  7965  ltexprlemrl  7967  ltexprlemru  7969  lteupri  7974  recexprlempr  7989  cauappcvgprlemm  8002  cauappcvgprlemopl  8003  cauappcvgprlemlol  8004  cauappcvgprlemopu  8005  cauappcvgprlemupu  8006  cauappcvgprlemloc  8009  cauappcvgprlemcl  8010  cauappcvgprlemladdfu  8011  cauappcvgprlemladdfl  8012  cauappcvgprlem2  8017  caucvgprlemm  8025  caucvgprlemopl  8026  caucvgprlemlol  8027  caucvgprlemopu  8028  caucvgprlemupu  8029  caucvgprlemloc  8032  caucvgprlemcl  8033  caucvgprlemladdfu  8034  caucvgprlem2  8037  caucvgprprlemml  8051  caucvgprprlemmu  8052  caucvgprprlemopl  8054  caucvgprprlemlol  8055  caucvgprprlemopu  8056  caucvgprprlemupu  8057  caucvgprprlemloc  8060  caucvgprprlemcl  8061  caucvgprprlem2  8067  suplocexprlemex  8079  suplocsrlem  8165  elrealeu  8186  rereceu  8246  axpre-suploclemres  8258  negf1o  8699  aptap  8968  receuap  8989  divvalap  8994  cju  9281  nn0ge2m1nn  9606  nnnegz  9626  elnnz  9633  elnn0z  9636  peano2z  9659  nn0n0n1ge2  9694  msqznn  9725  eluzaddi  9928  eluzsubi  9929  uzind4  9967  supinfneg  9974  infsupneg  9975  elnn1uz2  9986  uz2mulcl  9987  divfnzn  10000  nnrp  10043  rpaddcl  10057  rpmulcl  10058  rpdivcl  10059  rpgecl  10062  ge0p1rp  10065  elrpd  10073  ge0addcl  10362  ge0mulcl  10363  ge0xaddcl  10364  icoshftf1o  10372  peano2fzr  10420  uzsubsubfz  10430  fzsplit2  10433  fzsplit3  10436  elfznn  10438  fzss1  10447  fzss2  10448  fzp1elp1  10460  elfz1b  10475  elfz0fzfz0  10511  fz0fzelfz0  10512  difelfznle  10520  elfzofz  10548  nn0p1elfzo  10572  fzosplitsnm1  10605  ubmelm1fzo  10622  fzofzp1b  10624  fzosplitsn  10629  zsupcllemstep  10640  zsupcl  10642  infssfzcldc  10647  infssfzledc  10648  exbtwnz  10663  flqge0nn0  10706  flqge1nn  10707  zmodcl  10759  modqmuladdnn0  10783  modsumfzodifsn  10811  frec2uzf1od  10821  frec2uzisod  10822  frecuzrdgrrn  10823  frec2uzrdg  10824  frecuzrdgrcl  10825  frecuzrdgtcl  10827  frecuzrdgsuc  10829  frecuzrdgrclt  10830  frecuzrdgfunlem  10834  frecuzrdgtclt  10836  frecuzrdgsuctlem  10838  uzennn  10851  seq3fveq2  10890  seqfveq2g  10892  monoord  10900  iseqf1olemqcl  10914  iseqf1olemnab  10916  iseqf1olemab  10917  iseqf1olemqf1o  10921  seq3f1olemqsumkj  10926  seq3f1olemqsumk  10927  seq3id2  10941  exp3val  10956  expcl2lemap  10966  expclzaplem  10978  expge0  10990  expge1  10991  zsqcl2  11032  bcval4  11168  bcn1  11174  bccl2  11184  hashennnuni  11196  hashunlem  11222  hashdifpr  11239  zfz1isolem1  11270  seq3coll  11272  iswrdiz  11289  ccatsymb  11348  ccatrn  11355  ccat2s1fvwd  11393  swrds1  11418  swrdccat2  11421  swrdccatin2  11479  pfxccatin12lem2  11481  pfxccatin12lem3  11482  pfxccatin12  11483  pfxccat3  11484  pfxccat3a  11488  shftfn  11567  shftf  11573  recvguniq  11739  resqrexlemdecn  11756  rersqreu  11772  nn0abscl  11829  nnabscl  11844  abs2dif  11850  nn0maxcl  11969  climuni  12037  2clim  12045  climcn2  12053  summodclem2a  12126  fsum3  12132  fsum3cvg3  12141  fsumcl2lem  12143  fsumadd  12151  fisum0diag2  12192  fsummulc2  12193  fsumge0  12204  geolim2  12257  cvgratnnlemabsle  12272  cvgratz  12277  mertenslemi1  12280  prodmodclem3  12320  prodmodclem2a  12321  fprodeq0  12362  fprodge0  12382  eff2  12425  tanvalap  12453  zdvdsdc  12557  fzo0dvdseq  12602  oexpneg  12622  oddge22np1  12626  evennn02n  12627  evennn2n  12628  nno  12651  divalglemeunn  12666  divalglemex  12667  divalglemeuneg  12668  divalg  12669  bitsfzolem  12699  bitsinv1lem  12706  divgcdz  12726  bezoutlemmain  12753  bezoutlemmo  12761  bezoutlemeu  12762  bezoutlemle  12763  sqgcd  12784  uzwodc  12792  nninfctlemfo  12795  eucalgval2  12809  eucalglt  12813  lcmneg  12830  lcmgcdlem  12833  ncoprmgcdne1b  12845  prmind2  12876  prmdc  12886  sqnprm  12892  isprm5lem  12897  isprm5  12898  isprm6  12903  sqrt2irrlem  12917  pw2dvdseu  12924  sqpweven  12931  2sqpwodd  12932  sqrt2irrap  12936  qgt0numnn  12955  phicl2  12970  crth  12980  phimullem  12981  eulerthlem1  12983  eulerthlemh  12987  eulerthlemth  12988  hashgcdlem  12994  oddprm  13016  pythagtriplem6  13027  pythagtriplem11  13031  pythagtriplem13  13033  pythagtriplem19  13039  pclem0  13043  pcpremul  13050  pceu  13052  pc2dvds  13087  difsqpwdvds  13095  pcadd  13097  pockthlem  13113  pockthg  13114  1arith  13124  4sqlemffi  13153  4sqlem11  13158  4sqlem12  13159  4sqlem13m  13160  4sqlem14  13161  4sqlem17  13164  ballotfilemic  13228  ballotfilem1c  13229  ballotfilemrc  13252  ballotfilemth  13259  oddennn  13261  evenennn  13262  ennnfoneleminc  13280  ennnfonelemf1  13287  ennnfonelemen  13290  exmidunben  13295  ctinf  13299  ctiunctlemfo  13308  nninfdclemlt  13320  nninfdclemf1  13321  ptex  13595  imasaddfnlemg  13612  imasaddflemg  13614  mgmsscl  13658  sgrp0  13702  sgrp1  13703  hashfinmndnn  13722  ismndd  13727  mndpfo  13728  mhmf1o  13754  0mhm  13770  resmhm  13771  resmhm2  13772  resmhm2b  13773  mhmco  13774  gsumvallem2  13777  isgrpd2e  13802  grpinvf1o  13852  grpinvnzcl  13854  dfgrp3m  13881  mhmmnd  13896  ghmgrp  13898  mulgval  13902  mulgfng  13904  subgmulg  13968  issubg4m  13973  isnsg3  13987  nmzsubg  13990  ssnmz  13991  0nsg  13994  nsgid  13995  ghmnsgima  14048  ghmnsgpreima  14049  ghmf1  14053  kerf1ghm  14054  ghmf1o  14055  conjnmzb  14060  isabld  14079  cmnsubm  14089  ghmcmn  14108  ghmabl  14109  invghm  14110  gsumvalfi  14129  srgfcl  14251  srglmhm  14271  srgrmhm  14272  iscrngd  14320  ringsrg  14325  unitabl  14397  rhmf1o  14448  rhmco  14454  ringelnzr  14467  subrngringnsg  14486  subrgcrng  14506  subrgnzr  14523  resrhm  14529  unitrrg  14549  aprnzr  14572  aprlring  14573  drngnzr  14592  lssneln0  14683  rnglidlmsgrp  14806  quscrng  14842  expghmap  14914  mulgghm2  14915  znf1o  14958  znidom  14964  znidomb  14965  psrbaglesuppg  14980  psrbagcon  14985  tgtopon  15090  distopon  15111  epttop  15114  resttopon  15195  resttopon2  15202  cnco  15245  lmss  15270  txtopon  15286  uptx  15298  txdis1cn  15302  hmeocnv  15331  hmeof1o2  15332  hmeores  15339  hmeoco  15340  idhmeo  15341  txhmeo  15343  txswaphmeo  15345  psmetxrge0  15356  isxmet2d  15372  metres2  15405  xmetresbl  15464  comet  15523  bdxmet  15525  bdmet  15526  tgioo  15578  mulc1cncf  15613  mulcncflem  15631  cnrehmeocntop  15634  cnopnap  15635  dedekindeu  15647  dedekindicclemicc  15656  ivthinclemlm  15658  ivthinclemum  15659  ivthinclemlopn  15660  ivthinclemlr  15661  ivthinclemuopn  15662  ivthinclemur  15663  ivthinclemloc  15665  ivthinc  15667  ivthreinc  15669  dvfgg  15712  dvcjbr  15732  dvcj  15733  dvfre  15734  elplyr  15764  plyreres  15788  rplogbval  15970  sgmnncl  16016  mpodvdsmulf1o  16018  mersenne  16025  perfectlem2  16028  lgsfcl2  16039  lgsval2lem  16043  lgsmod  16059  lgsdirprm  16067  lgsne0  16071  gausslemma2dlem0h  16089  gausslemma2dlem1a  16091  gausslemma2dlem1f1o  16093  gausslemma2dlem4  16097  lgseisenlem1  16103  lgseisenlem2  16104  lgsquadlem1  16110  lgsquadlem2  16111  lgsquad2lem2  16115  2sqlem8  16156  2sqlem9  16157  structiedg0val  16195  ausgrumgrien  16325  usgredgreu  16371  uspgredg2vtxeu  16373  uspgredg2v  16376  usgredg2v  16379  usgr1e  16396  subuhgr  16427  subupgr  16428  subumgr  16429  subusgr  16430  vdegp1aid  16469  trlres  16545  clwwlkbp  16550  clwwlkccatlem  16555  s2elclwwlknon2  16591  clwwlknonex2lem2  16593  clwwlknonex2e  16595  bj-charfundcALT  16749  bj-nnord  16898  bj-inf2vnlem1  16910  pwf1oexmid  16943  nnsf  16953  nninfall  16957  nninfself  16961  exmidsbthrlem  16972  qdencn  16977