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  1765  sbequ1  1766  sbidm  1849  eqeu  2905  euind  2922  reuind  2940  eldifd  3137  eqssd  3170  ssrabdv  3232  elind  3318  dcun  3531  opm  4228  issod  4313  ordsucim  4493  onintonm  4510  ordtri2or2exmidlem  4519  en2lp  4547  ordwe  4569  sosng  4693  sotri2  5018  sotri3  5019  relssdmrn  5141  funun  5252  fnsng  5255  fnprg  5263  fntpg  5264  fntp  5265  fununi  5276  imain  5290  fnco  5316  f00  5399  f1ss  5419  f1ssr  5420  f1ssres  5422  f1f1orn  5464  foimacnv  5471  foun  5472  fun11iun  5474  sefvex  5528  dff3im  5653  fmpt  5658  ffnfv  5666  fmpt2d  5670  ffvresb  5671  fprg  5691  foco2  5745  fcof1  5774  fcofo  5775  fcof1o  5780  fliftf  5790  isoini2  5810  f1oiso  5817  moriotass  5849  fnoprabg  5966  f1ocnvd  6063  suppssfv  6069  suppssov1  6070  1stcof  6154  2ndcof  6155  1stconst  6212  2ndconst  6213  fo2ndf  6218  f1o2ndf1  6219  f1od2  6226  smores2  6285  tfrlem5  6305  tfrlemibfn  6319  tfr1onlembfn  6335  tfri1dALT  6342  tfrcllembfn  6348  nntri2  6485  eroveu  6616  elixpsn  6725  dom2lem  6762  xpf1o  6834  fidifsnen  6860  finexdc  6892  unfidisj  6911  f1finf1o  6936  fidcenumlemrks  6942  sbthlemi9  6954  supeuti  6983  infeuti  7018  casef1  7079  caseinl  7080  caseinr  7081  difinfsnlem  7088  ctmlemr  7097  ctm  7098  ctssdclemn0  7099  ctssdccl  7100  ctssdc  7102  enumctlemm  7103  nnnninf  7114  nninfwlpoimlemg  7163  en2other2  7185  exmidfodomrlemim  7190  pw1nel3  7220  cc2lem  7240  cc4f  7243  addclpi  7301  mulclpi  7302  nnppipi  7317  recmulnqg  7365  enq0ref  7407  nqnq0pi  7412  genipv  7483  addclpr  7511  nqprxx  7520  prmuloc  7540  mulclpr  7546  distrlem1prl  7556  distrlem1pru  7557  ltexprlempr  7582  ltexprlemrl  7584  ltexprlemru  7586  lteupri  7591  recexprlempr  7606  cauappcvgprlemm  7619  cauappcvgprlemopl  7620  cauappcvgprlemlol  7621  cauappcvgprlemopu  7622  cauappcvgprlemupu  7623  cauappcvgprlemloc  7626  cauappcvgprlemcl  7627  cauappcvgprlemladdfu  7628  cauappcvgprlemladdfl  7629  cauappcvgprlem2  7634  caucvgprlemm  7642  caucvgprlemopl  7643  caucvgprlemlol  7644  caucvgprlemopu  7645  caucvgprlemupu  7646  caucvgprlemloc  7649  caucvgprlemcl  7650  caucvgprlemladdfu  7651  caucvgprlem2  7654  caucvgprprlemml  7668  caucvgprprlemmu  7669  caucvgprprlemopl  7671  caucvgprprlemlol  7672  caucvgprprlemopu  7673  caucvgprprlemupu  7674  caucvgprprlemloc  7677  caucvgprprlemcl  7678  caucvgprprlem2  7684  suplocexprlemex  7696  suplocsrlem  7782  elrealeu  7803  rereceu  7863  axpre-suploclemres  7875  negf1o  8313  receuap  8599  divvalap  8603  cju  8889  nn0ge2m1nn  9207  nnnegz  9227  elnnz  9234  elnn0z  9237  peano2z  9260  nn0n0n1ge2  9294  msqznn  9324  eluzaddi  9525  eluzsubi  9526  uzind4  9559  supinfneg  9566  infsupneg  9567  elnn1uz2  9578  uz2mulcl  9579  divfnzn  9592  nnrp  9632  rpaddcl  9646  rpmulcl  9647  rpdivcl  9648  rpgecl  9651  ge0p1rp  9654  elrpd  9662  ge0addcl  9950  ge0mulcl  9951  ge0xaddcl  9952  icoshftf1o  9960  peano2fzr  10005  uzsubsubfz  10015  fzsplit2  10018  elfznn  10022  fzss1  10031  fzss2  10032  fzp1elp1  10043  elfz1b  10058  elfz0fzfz0  10094  fz0fzelfz0  10095  difelfznle  10103  elfzofz  10130  fzosplitsnm1  10177  ubmelm1fzo  10194  fzofzp1b  10196  fzosplitsn  10201  exbtwnz  10219  flqge0nn0  10261  flqge1nn  10262  zmodcl  10312  modqmuladdnn0  10336  modsumfzodifsn  10364  frec2uzf1od  10374  frec2uzisod  10375  frecuzrdgrrn  10376  frec2uzrdg  10377  frecuzrdgrcl  10378  frecuzrdgtcl  10380  frecuzrdgsuc  10382  frecuzrdgrclt  10383  frecuzrdgfunlem  10387  frecuzrdgtclt  10389  frecuzrdgsuctlem  10391  uzennn  10404  seq3fveq2  10437  monoord  10444  iseqf1olemqcl  10454  iseqf1olemnab  10456  iseqf1olemab  10457  iseqf1olemqf1o  10461  seq3f1olemqsumkj  10466  seq3f1olemqsumk  10467  seq3id2  10477  exp3val  10490  expcl2lemap  10500  expclzaplem  10512  expge0  10524  expge1  10525  zsqcl2  10565  bcval4  10698  bcn1  10704  bccl2  10714  hashennnuni  10725  hashunlem  10750  hashdifpr  10766  zfz1isolem1  10786  seq3coll  10788  shftfn  10799  shftf  10805  recvguniq  10970  resqrexlemdecn  10987  rersqreu  11003  nn0abscl  11060  nnabscl  11075  abs2dif  11081  climuni  11267  2clim  11275  climcn2  11283  summodclem2a  11355  fsum3  11361  fsum3cvg3  11370  fsumcl2lem  11372  fsumadd  11380  fisum0diag2  11421  fsummulc2  11422  fsumge0  11433  geolim2  11486  cvgratnnlemabsle  11501  cvgratz  11506  mertenslemi1  11509  prodmodclem3  11549  prodmodclem2a  11550  fprodeq0  11591  fprodge0  11611  eff2  11654  tanvalap  11682  zdvdsdc  11785  fzo0dvdseq  11828  oexpneg  11847  oddge22np1  11851  evennn02n  11852  evennn2n  11853  nno  11876  divalglemeunn  11891  divalglemex  11892  divalglemeuneg  11893  divalg  11894  zsupcllemstep  11911  zsupcl  11913  divgcdz  11937  bezoutlemmain  11964  bezoutlemmo  11972  bezoutlemeu  11973  bezoutlemle  11974  sqgcd  11995  uzwodc  12003  eucalgval2  12018  eucalglt  12022  lcmcllem  12032  lcmledvds  12035  lcmneg  12039  lcmgcdlem  12042  ncoprmgcdne1b  12054  prmind2  12085  prmdc  12095  sqnprm  12101  isprm5lem  12106  isprm5  12107  isprm6  12112  sqrt2irrlem  12126  pw2dvdseu  12133  sqpweven  12140  2sqpwodd  12141  sqrt2irrap  12145  qgt0numnn  12164  phicl2  12179  hashdvds  12186  crth  12189  phimullem  12190  eulerthlem1  12192  eulerthlemh  12196  eulerthlemth  12197  hashgcdlem  12203  oddprm  12224  pythagtriplem6  12235  pythagtriplem11  12239  pythagtriplem13  12241  pythagtriplem19  12247  pclem0  12251  pcpremul  12258  pceu  12260  pc2dvds  12294  difsqpwdvds  12302  pcadd  12304  pockthlem  12319  pockthg  12320  1arith  12330  oddennn  12358  evenennn  12359  ennnfoneleminc  12377  ennnfonelemf1  12384  ennnfonelemen  12387  exmidunben  12392  ctinf  12396  ctiunctlemfo  12405  nninfdclemlt  12417  nninfdclemf1  12418  mgmsscl  12644  sgrp0  12679  sgrp1  12680  hashfinmndnn  12697  ismndd  12702  mndpfo  12703  mhmf1o  12722  0mhm  12733  mhmco  12734  isgrpd2e  12756  grpinvf1o  12799  grpinvnzcl  12801  dfgrp3m  12828  mhmmnd  12839  ghmgrp  12841  mulgval  12845  mulgfng  12846  isabld  12898  srgfcl  12949  srglmhm  12969  srgrmhm  12970  iscrngd  13013  ringsrg  13016  tgtopon  13117  distopon  13138  epttop  13141  resttopon  13222  resttopon2  13229  cnco  13272  lmss  13297  txtopon  13313  uptx  13325  txdis1cn  13329  hmeocnv  13358  hmeof1o2  13359  hmeores  13366  hmeoco  13367  idhmeo  13368  txhmeo  13370  txswaphmeo  13372  psmetxrge0  13383  isxmet2d  13399  metres2  13432  xmetresbl  13491  comet  13550  bdxmet  13552  bdmet  13553  tgioo  13597  mulc1cncf  13627  mulcncflem  13641  cnrehmeocntop  13644  cnopnap  13645  dedekindeu  13652  dedekindicclemicc  13661  ivthinclemlm  13663  ivthinclemum  13664  ivthinclemlopn  13665  ivthinclemlr  13666  ivthinclemuopn  13667  ivthinclemur  13668  ivthinclemloc  13670  ivthinc  13672  dvfgg  13708  dvcjbr  13723  dvcj  13724  dvfre  13725  rplogbval  13914  lgsfcl2  13958  lgsval2lem  13962  lgsmod  13978  lgsdirprm  13986  lgsne0  13990  2sqlem8  14010  2sqlem9  14011  bj-charfundcALT  14101  bj-nnord  14250  bj-inf2vnlem1  14262  pwf1oexmid  14289  nnsf  14295  nninfall  14299  nninfself  14303  exmidsbthrlem  14311  qdencn  14316