Theorem sylanbrc 415

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 304	. 2 |- ( ph -> ( ps /\ ch ) )
4		sylanbrc.3	. 2 |- ( th <-> ( ps /\ ch ) )
5	3, 4	sylibr 133	1 |- ( ph -> th )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  sb2  1760  sbequ1  1761  sbidm  1844  eqeu  2900  euind  2917  reuind  2935  eldifd  3131  eqssd  3164  ssrabdv  3226  elind  3312  dcun  3525  opm  4219  issod  4304  ordsucim  4484  onintonm  4501  ordtri2or2exmidlem  4510  en2lp  4538  ordwe  4560  sosng  4684  sotri2  5008  sotri3  5009  relssdmrn  5131  funun  5242  fnsng  5245  fnprg  5253  fntpg  5254  fntp  5255  fununi  5266  imain  5280  fnco  5306  f00  5389  f1ss  5409  f1ssr  5410  f1ssres  5412  f1f1orn  5453  foimacnv  5460  foun  5461  fun11iun  5463  sefvex  5517  dff3im  5641  fmpt  5646  ffnfv  5654  fmpt2d  5658  ffvresb  5659  fprg  5679  foco2  5733  fcof1  5762  fcofo  5763  fcof1o  5768  fliftf  5778  isoini2  5798  f1oiso  5805  moriotass  5837  fnoprabg  5954  f1ocnvd  6051  suppssfv  6057  suppssov1  6058  1stcof  6142  2ndcof  6143  1stconst  6200  2ndconst  6201  fo2ndf  6206  f1o2ndf1  6207  f1od2  6214  smores2  6273  tfrlem5  6293  tfrlemibfn  6307  tfr1onlembfn  6323  tfri1dALT  6330  tfrcllembfn  6336  nntri2  6473  eroveu  6604  elixpsn  6713  dom2lem  6750  xpf1o  6822  fidifsnen  6848  finexdc  6880  unfidisj  6899  f1finf1o  6924  fidcenumlemrks  6930  sbthlemi9  6942  supeuti  6971  infeuti  7006  casef1  7067  caseinl  7068  caseinr  7069  difinfsnlem  7076  ctmlemr  7085  ctm  7086  ctssdclemn0  7087  ctssdccl  7088  ctssdc  7090  enumctlemm  7091  nnnninf  7102  nninfwlpoimlemg  7151  en2other2  7173  exmidfodomrlemim  7178  pw1nel3  7208  cc2lem  7228  cc4f  7231  addclpi  7289  mulclpi  7290  nnppipi  7305  recmulnqg  7353  enq0ref  7395  nqnq0pi  7400  genipv  7471  addclpr  7499  nqprxx  7508  prmuloc  7528  mulclpr  7534  distrlem1prl  7544  distrlem1pru  7545  ltexprlempr  7570  ltexprlemrl  7572  ltexprlemru  7574  lteupri  7579  recexprlempr  7594  cauappcvgprlemm  7607  cauappcvgprlemopl  7608  cauappcvgprlemlol  7609  cauappcvgprlemopu  7610  cauappcvgprlemupu  7611  cauappcvgprlemloc  7614  cauappcvgprlemcl  7615  cauappcvgprlemladdfu  7616  cauappcvgprlemladdfl  7617  cauappcvgprlem2  7622  caucvgprlemm  7630  caucvgprlemopl  7631  caucvgprlemlol  7632  caucvgprlemopu  7633  caucvgprlemupu  7634  caucvgprlemloc  7637  caucvgprlemcl  7638  caucvgprlemladdfu  7639  caucvgprlem2  7642  caucvgprprlemml  7656  caucvgprprlemmu  7657  caucvgprprlemopl  7659  caucvgprprlemlol  7660  caucvgprprlemopu  7661  caucvgprprlemupu  7662  caucvgprprlemloc  7665  caucvgprprlemcl  7666  caucvgprprlem2  7672  suplocexprlemex  7684  suplocsrlem  7770  elrealeu  7791  rereceu  7851  axpre-suploclemres  7863  negf1o  8301  receuap  8587  divvalap  8591  cju  8877  nn0ge2m1nn  9195  nnnegz  9215  elnnz  9222  elnn0z  9225  peano2z  9248  nn0n0n1ge2  9282  msqznn  9312  eluzaddi  9513  eluzsubi  9514  uzind4  9547  supinfneg  9554  infsupneg  9555  elnn1uz2  9566  uz2mulcl  9567  divfnzn  9580  nnrp  9620  rpaddcl  9634  rpmulcl  9635  rpdivcl  9636  rpgecl  9639  ge0p1rp  9642  elrpd  9650  ge0addcl  9938  ge0mulcl  9939  ge0xaddcl  9940  icoshftf1o  9948  peano2fzr  9993  uzsubsubfz  10003  fzsplit2  10006  elfznn  10010  fzss1  10019  fzss2  10020  fzp1elp1  10031  elfz1b  10046  elfz0fzfz0  10082  fz0fzelfz0  10083  difelfznle  10091  elfzofz  10118  fzosplitsnm1  10165  ubmelm1fzo  10182  fzofzp1b  10184  fzosplitsn  10189  exbtwnz  10207  flqge0nn0  10249  flqge1nn  10250  zmodcl  10300  modqmuladdnn0  10324  modsumfzodifsn  10352  frec2uzf1od  10362  frec2uzisod  10363  frecuzrdgrrn  10364  frec2uzrdg  10365  frecuzrdgrcl  10366  frecuzrdgtcl  10368  frecuzrdgsuc  10370  frecuzrdgrclt  10371  frecuzrdgfunlem  10375  frecuzrdgtclt  10377  frecuzrdgsuctlem  10379  uzennn  10392  seq3fveq2  10425  monoord  10432  iseqf1olemqcl  10442  iseqf1olemnab  10444  iseqf1olemab  10445  iseqf1olemqf1o  10449  seq3f1olemqsumkj  10454  seq3f1olemqsumk  10455  seq3id2  10465  exp3val  10478  expcl2lemap  10488  expclzaplem  10500  expge0  10512  expge1  10513  zsqcl2  10553  bcval4  10686  bcn1  10692  bccl2  10702  hashennnuni  10713  hashunlem  10739  hashdifpr  10755  zfz1isolem1  10775  seq3coll  10777  shftfn  10788  shftf  10794  recvguniq  10959  resqrexlemdecn  10976  rersqreu  10992  nn0abscl  11049  nnabscl  11064  abs2dif  11070  climuni  11256  2clim  11264  climcn2  11272  summodclem2a  11344  fsum3  11350  fsum3cvg3  11359  fsumcl2lem  11361  fsumadd  11369  fisum0diag2  11410  fsummulc2  11411  fsumge0  11422  geolim2  11475  cvgratnnlemabsle  11490  cvgratz  11495  mertenslemi1  11498  prodmodclem3  11538  prodmodclem2a  11539  fprodeq0  11580  fprodge0  11600  eff2  11643  tanvalap  11671  zdvdsdc  11774  fzo0dvdseq  11817  oexpneg  11836  oddge22np1  11840  evennn02n  11841  evennn2n  11842  nno  11865  divalglemeunn  11880  divalglemex  11881  divalglemeuneg  11882  divalg  11883  zsupcllemstep  11900  zsupcl  11902  divgcdz  11926  bezoutlemmain  11953  bezoutlemmo  11961  bezoutlemeu  11962  bezoutlemle  11963  sqgcd  11984  uzwodc  11992  eucalgval2  12007  eucalglt  12011  lcmcllem  12021  lcmledvds  12024  lcmneg  12028  lcmgcdlem  12031  ncoprmgcdne1b  12043  prmind2  12074  prmdc  12084  sqnprm  12090  isprm5lem  12095  isprm5  12096  isprm6  12101  sqrt2irrlem  12115  pw2dvdseu  12122  sqpweven  12129  2sqpwodd  12130  sqrt2irrap  12134  qgt0numnn  12153  phicl2  12168  hashdvds  12175  crth  12178  phimullem  12179  eulerthlem1  12181  eulerthlemh  12185  eulerthlemth  12186  hashgcdlem  12192  oddprm  12213  pythagtriplem6  12224  pythagtriplem11  12228  pythagtriplem13  12230  pythagtriplem19  12236  pclem0  12240  pcpremul  12247  pceu  12249  pc2dvds  12283  difsqpwdvds  12291  pcadd  12293  pockthlem  12308  pockthg  12309  1arith  12319  oddennn  12347  evenennn  12348  ennnfoneleminc  12366  ennnfonelemf1  12373  ennnfonelemen  12376  exmidunben  12381  ctinf  12385  ctiunctlemfo  12394  nninfdclemlt  12406  nninfdclemf1  12407  mgmsscl  12615  sgrp0  12650  sgrp1  12651  hashfinmndnn  12668  ismndd  12673  mndpfo  12674  mhmf1o  12693  0mhm  12704  mhmco  12705  isgrpd2e  12726  grpinvf1o  12769  grpinvnzcl  12771  tgtopon  12860  distopon  12881  epttop  12884  resttopon  12965  resttopon2  12972  cnco  13015  lmss  13040  txtopon  13056  uptx  13068  txdis1cn  13072  hmeocnv  13101  hmeof1o2  13102  hmeores  13109  hmeoco  13110  idhmeo  13111  txhmeo  13113  txswaphmeo  13115  psmetxrge0  13126  isxmet2d  13142  metres2  13175  xmetresbl  13234  comet  13293  bdxmet  13295  bdmet  13296  tgioo  13340  mulc1cncf  13370  mulcncflem  13384  cnrehmeocntop  13387  cnopnap  13388  dedekindeu  13395  dedekindicclemicc  13404  ivthinclemlm  13406  ivthinclemum  13407  ivthinclemlopn  13408  ivthinclemlr  13409  ivthinclemuopn  13410  ivthinclemur  13411  ivthinclemloc  13413  ivthinc  13415  dvfgg  13451  dvcjbr  13466  dvcj  13467  dvfre  13468  rplogbval  13657  lgsfcl2  13701  lgsval2lem  13705  lgsmod  13721  lgsdirprm  13729  lgsne0  13733  2sqlem8  13753  2sqlem9  13754  bj-charfundcALT  13844  bj-nnord  13993  bj-inf2vnlem1  14005  pwf1oexmid  14032  nnsf  14038  nninfall  14042  nninfself  14046  exmidsbthrlem  14054  qdencn  14059