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  934  sb2  1781  sbequ1  1782  sbidm  1865  eqeu  2934  euind  2951  reuind  2969  eldifd  3167  eqssd  3200  ssrabdv  3262  elind  3348  dcun  3560  opm  4267  issod  4354  ordsucim  4536  onintonm  4553  ordtri2or2exmidlem  4562  en2lp  4590  ordwe  4612  sosng  4736  sotri2  5067  sotri3  5068  relssdmrn  5190  funun  5302  fnsng  5305  fnprg  5313  fntpg  5314  fntp  5315  fununi  5326  imain  5340  fnco  5366  f00  5449  f1ss  5469  f1ssr  5470  f1ssres  5472  f1f1orn  5515  foimacnv  5522  foun  5523  fun11iun  5525  sefvex  5579  dff3im  5707  fmpt  5712  ffnfv  5720  fmpt2d  5724  ffvresb  5725  fprg  5745  foco2  5800  fcof1  5830  fcofo  5831  fcof1o  5836  fliftf  5846  isoini2  5866  f1oiso  5873  moriotass  5906  fnoprabg  6023  f1ocnvd  6125  suppssfv  6131  suppssov1  6132  1stcof  6221  2ndcof  6222  1stconst  6279  2ndconst  6280  fo2ndf  6285  f1o2ndf1  6286  f1od2  6293  smores2  6352  tfrlem5  6372  tfrlemibfn  6386  tfr1onlembfn  6402  tfri1dALT  6409  tfrcllembfn  6415  nntri2  6552  eroveu  6685  elixpsn  6794  dom2lem  6831  xpf1o  6905  fidifsnen  6931  finexdc  6963  unfidisj  6983  f1finf1o  7013  fidcenumlemrks  7019  sbthlemi9  7031  supeuti  7060  infeuti  7095  casef1  7156  caseinl  7157  caseinr  7158  difinfsnlem  7165  ctmlemr  7174  ctm  7175  ctssdclemn0  7176  ctssdccl  7177  ctssdc  7179  enumctlemm  7180  nnnninf  7192  nninfwlpoimlemg  7241  en2other2  7263  exmidfodomrlemim  7268  pw1nel3  7298  dftap2  7318  cc2lem  7333  cc4f  7336  addclpi  7394  mulclpi  7395  nnppipi  7410  recmulnqg  7458  enq0ref  7500  nqnq0pi  7505  genipv  7576  addclpr  7604  nqprxx  7613  prmuloc  7633  mulclpr  7639  distrlem1prl  7649  distrlem1pru  7650  ltexprlempr  7675  ltexprlemrl  7677  ltexprlemru  7679  lteupri  7684  recexprlempr  7699  cauappcvgprlemm  7712  cauappcvgprlemopl  7713  cauappcvgprlemlol  7714  cauappcvgprlemopu  7715  cauappcvgprlemupu  7716  cauappcvgprlemloc  7719  cauappcvgprlemcl  7720  cauappcvgprlemladdfu  7721  cauappcvgprlemladdfl  7722  cauappcvgprlem2  7727  caucvgprlemm  7735  caucvgprlemopl  7736  caucvgprlemlol  7737  caucvgprlemopu  7738  caucvgprlemupu  7739  caucvgprlemloc  7742  caucvgprlemcl  7743  caucvgprlemladdfu  7744  caucvgprlem2  7747  caucvgprprlemml  7761  caucvgprprlemmu  7762  caucvgprprlemopl  7764  caucvgprprlemlol  7765  caucvgprprlemopu  7766  caucvgprprlemupu  7767  caucvgprprlemloc  7770  caucvgprprlemcl  7771  caucvgprprlem2  7777  suplocexprlemex  7789  suplocsrlem  7875  elrealeu  7896  rereceu  7956  axpre-suploclemres  7968  negf1o  8408  aptap  8677  receuap  8696  divvalap  8701  cju  8988  nn0ge2m1nn  9309  nnnegz  9329  elnnz  9336  elnn0z  9339  peano2z  9362  nn0n0n1ge2  9396  msqznn  9426  eluzaddi  9628  eluzsubi  9629  uzind4  9662  supinfneg  9669  infsupneg  9670  elnn1uz2  9681  uz2mulcl  9682  divfnzn  9695  nnrp  9738  rpaddcl  9752  rpmulcl  9753  rpdivcl  9754  rpgecl  9757  ge0p1rp  9760  elrpd  9768  ge0addcl  10056  ge0mulcl  10057  ge0xaddcl  10058  icoshftf1o  10066  peano2fzr  10112  uzsubsubfz  10122  fzsplit2  10125  elfznn  10129  fzss1  10138  fzss2  10139  fzp1elp1  10150  elfz1b  10165  elfz0fzfz0  10201  fz0fzelfz0  10202  difelfznle  10210  elfzofz  10238  fzosplitsnm1  10285  ubmelm1fzo  10302  fzofzp1b  10304  fzosplitsn  10309  zsupcllemstep  10319  zsupcl  10321  exbtwnz  10340  flqge0nn0  10383  flqge1nn  10384  zmodcl  10436  modqmuladdnn0  10460  modsumfzodifsn  10488  frec2uzf1od  10498  frec2uzisod  10499  frecuzrdgrrn  10500  frec2uzrdg  10501  frecuzrdgrcl  10502  frecuzrdgtcl  10504  frecuzrdgsuc  10506  frecuzrdgrclt  10507  frecuzrdgfunlem  10511  frecuzrdgtclt  10513  frecuzrdgsuctlem  10515  uzennn  10528  seq3fveq2  10567  seqfveq2g  10569  monoord  10577  iseqf1olemqcl  10591  iseqf1olemnab  10593  iseqf1olemab  10594  iseqf1olemqf1o  10598  seq3f1olemqsumkj  10603  seq3f1olemqsumk  10604  seq3id2  10618  exp3val  10633  expcl2lemap  10643  expclzaplem  10655  expge0  10667  expge1  10668  zsqcl2  10709  bcval4  10844  bcn1  10850  bccl2  10860  hashennnuni  10871  hashunlem  10896  hashdifpr  10912  zfz1isolem1  10932  seq3coll  10934  iswrdiz  10942  shftfn  10989  shftf  10995  recvguniq  11160  resqrexlemdecn  11177  rersqreu  11193  nn0abscl  11250  nnabscl  11265  abs2dif  11271  nn0maxcl  11390  climuni  11458  2clim  11466  climcn2  11474  summodclem2a  11546  fsum3  11552  fsum3cvg3  11561  fsumcl2lem  11563  fsumadd  11571  fisum0diag2  11612  fsummulc2  11613  fsumge0  11624  geolim2  11677  cvgratnnlemabsle  11692  cvgratz  11697  mertenslemi1  11700  prodmodclem3  11740  prodmodclem2a  11741  fprodeq0  11782  fprodge0  11802  eff2  11845  tanvalap  11873  zdvdsdc  11977  fzo0dvdseq  12022  oexpneg  12042  oddge22np1  12046  evennn02n  12047  evennn2n  12048  nno  12071  divalglemeunn  12086  divalglemex  12087  divalglemeuneg  12088  divalg  12089  bitsfzolem  12118  divgcdz  12138  bezoutlemmain  12165  bezoutlemmo  12173  bezoutlemeu  12174  bezoutlemle  12175  sqgcd  12196  uzwodc  12204  nninfctlemfo  12207  eucalgval2  12221  eucalglt  12225  lcmneg  12242  lcmgcdlem  12245  ncoprmgcdne1b  12257  prmind2  12288  prmdc  12298  sqnprm  12304  isprm5lem  12309  isprm5  12310  isprm6  12315  sqrt2irrlem  12329  pw2dvdseu  12336  sqpweven  12343  2sqpwodd  12344  sqrt2irrap  12348  qgt0numnn  12367  phicl2  12382  hashdvds  12389  crth  12392  phimullem  12393  eulerthlem1  12395  eulerthlemh  12399  eulerthlemth  12400  hashgcdlem  12406  oddprm  12428  pythagtriplem6  12439  pythagtriplem11  12443  pythagtriplem13  12445  pythagtriplem19  12451  pclem0  12455  pcpremul  12462  pceu  12464  pc2dvds  12499  difsqpwdvds  12507  pcadd  12509  pockthlem  12525  pockthg  12526  1arith  12536  4sqlemffi  12565  4sqlem11  12570  4sqlem12  12571  4sqlem13m  12572  4sqlem14  12573  4sqlem17  12576  oddennn  12609  evenennn  12610  ennnfoneleminc  12628  ennnfonelemf1  12635  ennnfonelemen  12638  exmidunben  12643  ctinf  12647  ctiunctlemfo  12656  nninfdclemlt  12668  nninfdclemf1  12669  ptex  12935  imasaddfnlemg  12957  imasaddflemg  12959  mgmsscl  13004  sgrp0  13053  sgrp1  13054  hashfinmndnn  13073  ismndd  13078  mndpfo  13079  mhmf1o  13102  0mhm  13118  resmhm  13119  resmhm2  13120  resmhm2b  13121  mhmco  13122  gsumvallem2  13125  isgrpd2e  13152  grpinvf1o  13202  grpinvnzcl  13204  dfgrp3m  13231  mhmmnd  13246  ghmgrp  13248  mulgval  13252  mulgfng  13254  subgmulg  13318  issubg4m  13323  isnsg3  13337  nmzsubg  13340  ssnmz  13341  0nsg  13344  nsgid  13345  ghmnsgima  13398  ghmnsgpreima  13399  ghmf1  13403  kerf1ghm  13404  ghmf1o  13405  conjnmzb  13410  isabld  13429  ghmcmn  13457  ghmabl  13458  invghm  13459  srgfcl  13529  srglmhm  13549  srgrmhm  13550  iscrngd  13598  ringsrg  13603  unitabl  13673  rhmf1o  13724  rhmco  13730  ringelnzr  13743  subrngringnsg  13761  subrgcrng  13781  subrgnzr  13798  resrhm  13804  unitrrg  13823  lssneln0  13930  rnglidlmsgrp  14053  quscrng  14089  expghmap  14163  mulgghm2  14164  znf1o  14207  znidom  14213  znidomb  14214  psrbaglesuppg  14226  tgtopon  14302  distopon  14323  epttop  14326  resttopon  14407  resttopon2  14414  cnco  14457  lmss  14482  txtopon  14498  uptx  14510  txdis1cn  14514  hmeocnv  14543  hmeof1o2  14544  hmeores  14551  hmeoco  14552  idhmeo  14553  txhmeo  14555  txswaphmeo  14557  psmetxrge0  14568  isxmet2d  14584  metres2  14617  xmetresbl  14676  comet  14735  bdxmet  14737  bdmet  14738  tgioo  14790  mulc1cncf  14825  mulcncflem  14843  cnrehmeocntop  14846  cnopnap  14847  dedekindeu  14859  dedekindicclemicc  14868  ivthinclemlm  14870  ivthinclemum  14871  ivthinclemlopn  14872  ivthinclemlr  14873  ivthinclemuopn  14874  ivthinclemur  14875  ivthinclemloc  14877  ivthinc  14879  ivthreinc  14881  dvfgg  14924  dvcjbr  14944  dvcj  14945  dvfre  14946  elplyr  14976  plyreres  15000  rplogbval  15181  sgmnncl  15224  mpodvdsmulf1o  15226  mersenne  15233  perfectlem2  15236  lgsfcl2  15247  lgsval2lem  15251  lgsmod  15267  lgsdirprm  15275  lgsne0  15279  gausslemma2dlem0h  15297  gausslemma2dlem1a  15299  gausslemma2dlem1f1o  15301  gausslemma2dlem4  15305  lgseisenlem1  15311  lgseisenlem2  15312  lgsquadlem1  15318  lgsquadlem2  15319  lgsquad2lem2  15323  2sqlem8  15364  2sqlem9  15365  bj-charfundcALT  15455  bj-nnord  15604  bj-inf2vnlem1  15616  pwf1oexmid  15644  nnsf  15649  nninfall  15653  nninfself  15657  exmidsbthrlem  15666  qdencn  15671