Theorem sylanbrc 413

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  1740  sbequ1  1741  sbidm  1823  eqeu  2854  euind  2871  reuind  2889  eldifd  3081  eqssd  3114  ssrabdv  3176  elind  3261  dcun  3473  opm  4156  issod  4241  ordsucim  4416  onintonm  4433  ordtri2or2exmidlem  4441  en2lp  4469  ordwe  4490  sosng  4612  sotri2  4936  sotri3  4937  relssdmrn  5059  funun  5167  fnsng  5170  fnprg  5178  fntpg  5179  fntp  5180  fununi  5191  imain  5205  fnco  5231  f00  5314  f1ss  5334  f1ssr  5335  f1ssres  5337  f1f1orn  5378  foimacnv  5385  foun  5386  fun11iun  5388  sefvex  5442  dff3im  5565  fmpt  5570  ffnfv  5578  fmpt2d  5582  ffvresb  5583  fprg  5603  foco2  5655  fcof1  5684  fcofo  5685  fcof1o  5690  fliftf  5700  isoini2  5720  f1oiso  5727  moriotass  5758  fnoprabg  5872  f1ocnvd  5972  suppssfv  5978  suppssov1  5979  1stcof  6061  2ndcof  6062  1stconst  6118  2ndconst  6119  fo2ndf  6124  f1o2ndf1  6125  f1od2  6132  smores2  6191  tfrlem5  6211  tfrlemibfn  6225  tfr1onlembfn  6241  tfri1dALT  6248  tfrcllembfn  6254  nntri2  6390  eroveu  6520  elixpsn  6629  dom2lem  6666  xpf1o  6738  fidifsnen  6764  finexdc  6796  unfidisj  6810  f1finf1o  6835  fidcenumlemrks  6841  sbthlemi9  6853  supeuti  6881  infeuti  6916  casef1  6975  caseinl  6976  caseinr  6977  difinfsnlem  6984  ctmlemr  6993  ctm  6994  ctssdclemn0  6995  ctssdccl  6996  ctssdc  6998  enumctlemm  6999  nnnninf  7023  en2other2  7052  exmidfodomrlemim  7057  addclpi  7135  mulclpi  7136  nnppipi  7151  recmulnqg  7199  enq0ref  7241  nqnq0pi  7246  genipv  7317  addclpr  7345  nqprxx  7354  prmuloc  7374  mulclpr  7380  distrlem1prl  7390  distrlem1pru  7391  ltexprlempr  7416  ltexprlemrl  7418  ltexprlemru  7420  lteupri  7425  recexprlempr  7440  cauappcvgprlemm  7453  cauappcvgprlemopl  7454  cauappcvgprlemlol  7455  cauappcvgprlemopu  7456  cauappcvgprlemupu  7457  cauappcvgprlemloc  7460  cauappcvgprlemcl  7461  cauappcvgprlemladdfu  7462  cauappcvgprlemladdfl  7463  cauappcvgprlem2  7468  caucvgprlemm  7476  caucvgprlemopl  7477  caucvgprlemlol  7478  caucvgprlemopu  7479  caucvgprlemupu  7480  caucvgprlemloc  7483  caucvgprlemcl  7484  caucvgprlemladdfu  7485  caucvgprlem2  7488  caucvgprprlemml  7502  caucvgprprlemmu  7503  caucvgprprlemopl  7505  caucvgprprlemlol  7506  caucvgprprlemopu  7507  caucvgprprlemupu  7508  caucvgprprlemloc  7511  caucvgprprlemcl  7512  caucvgprprlem2  7518  suplocexprlemex  7530  suplocsrlem  7616  elrealeu  7637  rereceu  7697  axpre-suploclemres  7709  negf1o  8144  receuap  8430  divvalap  8434  cju  8719  nn0ge2m1nn  9037  nnnegz  9057  elnnz  9064  elnn0z  9067  peano2z  9090  nn0n0n1ge2  9121  msqznn  9151  eluzaddi  9352  eluzsubi  9353  uzind4  9383  supinfneg  9390  infsupneg  9391  elnn1uz2  9401  uz2mulcl  9402  divfnzn  9413  nnrp  9451  rpaddcl  9465  rpmulcl  9466  rpdivcl  9467  rpgecl  9470  ge0p1rp  9473  elrpd  9481  ge0addcl  9764  ge0mulcl  9765  ge0xaddcl  9766  icoshftf1o  9774  peano2fzr  9817  uzsubsubfz  9827  fzsplit2  9830  elfznn  9834  fzss1  9843  fzss2  9844  fzp1elp1  9855  elfz1b  9870  elfz0fzfz0  9903  fz0fzelfz0  9904  difelfznle  9912  elfzofz  9939  fzosplitsnm1  9986  ubmelm1fzo  10003  fzofzp1b  10005  fzosplitsn  10010  exbtwnz  10028  flqge0nn0  10066  flqge1nn  10067  zmodcl  10117  modqmuladdnn0  10141  modsumfzodifsn  10169  frec2uzf1od  10179  frec2uzisod  10180  frecuzrdgrrn  10181  frec2uzrdg  10182  frecuzrdgrcl  10183  frecuzrdgtcl  10185  frecuzrdgsuc  10187  frecuzrdgrclt  10188  frecuzrdgfunlem  10192  frecuzrdgtclt  10194  frecuzrdgsuctlem  10196  uzennn  10209  seq3fveq2  10242  monoord  10249  iseqf1olemqcl  10259  iseqf1olemnab  10261  iseqf1olemab  10262  iseqf1olemqf1o  10266  seq3f1olemqsumkj  10271  seq3f1olemqsumk  10272  seq3id2  10282  exp3val  10295  expcl2lemap  10305  expclzaplem  10317  expge0  10329  expge1  10330  zsqcl2  10370  bcval4  10498  bcn1  10504  bccl2  10514  hashennnuni  10525  hashunlem  10550  hashdifpr  10566  zfz1isolem1  10583  seq3coll  10585  shftfn  10596  shftf  10602  recvguniq  10767  resqrexlemdecn  10784  rersqreu  10800  nn0abscl  10857  nnabscl  10872  abs2dif  10878  climuni  11062  2clim  11070  climcn2  11078  summodclem2a  11150  fsum3  11156  fsum3cvg3  11165  fsumcl2lem  11167  fsumadd  11175  fisum0diag2  11216  fsummulc2  11217  fsumge0  11228  geolim2  11281  cvgratnnlemabsle  11296  cvgratz  11301  mertenslemi1  11304  prodmodclem3  11344  prodmodclem2a  11345  eff2  11386  tanvalap  11415  zdvdsdc  11514  fzo0dvdseq  11555  oexpneg  11574  oddge22np1  11578  evennn02n  11579  evennn2n  11580  nno  11603  divalglemeunn  11618  divalglemex  11619  divalglemeuneg  11620  divalg  11621  zsupcllemstep  11638  zsupcl  11640  divgcdz  11660  bezoutlemmain  11686  bezoutlemmo  11694  bezoutlemeu  11695  bezoutlemle  11696  sqgcd  11717  eucalgval2  11734  eucalglt  11738  lcmcllem  11748  lcmledvds  11751  lcmneg  11755  lcmgcdlem  11758  ncoprmgcdne1b  11770  prmind2  11801  sqnprm  11816  isprm6  11825  sqrt2irrlem  11839  pw2dvdseu  11846  sqpweven  11853  2sqpwodd  11854  sqrt2irrap  11858  qgt0numnn  11877  phicl2  11890  hashdvds  11897  crth  11900  phimullem  11901  hashgcdlem  11903  oddennn  11905  evenennn  11906  ennnfoneleminc  11924  ennnfonelemf1  11931  ennnfonelemen  11934  exmidunben  11939  ctinf  11943  ctiunctlemfo  11952  tgtopon  12235  distopon  12256  epttop  12259  resttopon  12340  resttopon2  12347  cnco  12390  lmss  12415  txtopon  12431  uptx  12443  txdis1cn  12447  hmeocnv  12476  hmeof1o2  12477  hmeores  12484  hmeoco  12485  idhmeo  12486  txhmeo  12488  txswaphmeo  12490  psmetxrge0  12501  isxmet2d  12517  metres2  12550  xmetresbl  12609  comet  12668  bdxmet  12670  bdmet  12671  tgioo  12715  mulc1cncf  12745  mulcncflem  12759  cnrehmeocntop  12762  cnopnap  12763  dedekindeu  12770  dedekindicclemicc  12779  ivthinclemlm  12781  ivthinclemum  12782  ivthinclemlopn  12783  ivthinclemlr  12784  ivthinclemuopn  12785  ivthinclemur  12786  ivthinclemloc  12788  ivthinc  12790  dvfgg  12826  dvcjbr  12841  dvcj  12842  dvfre  12843  bj-nnord  13156  bj-inf2vnlem1  13168  pwf1oexmid  13194  nnsf  13199  nninfall  13204  nninfself  13209  exmidsbthrlem  13217  qdencn  13222