Theorem syl6bbr 196

Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
syl6bbr.1	|- ( ph -> ( ps <-> ch ) )
syl6bbr.2	|- ( th <-> ch )

Assertion

Ref	Expression
syl6bbr	|- ( ph -> ( ps <-> th ) )

Proof of Theorem syl6bbr

Step	Hyp	Ref	Expression
1		syl6bbr.1	. 2 |- ( ph -> ( ps <-> ch ) )
2		syl6bbr.2	. . 3 |- ( th <-> ch )
3	2	bicomi 130	. 2 |- ( ch <-> th )
4	1, 3	syl6bb 194	1 |- ( ph -> ( ps <-> th ) )

Syntax hints:   -> wi 4   <-> wb 103

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  3bitr4g  221  bibi2i  225  equsalh  1654  eueq3dc  2766  sbcel12g  2921  sbceqg  2922  sbcnel12g  2923  reldisj  3295  r19.3rm  3330  rabxp  4398  elrng  4544  iss  4674  eliniseg  4715  fcnvres  5093  dffv3g  5194  funimass4  5245  fndmdif  5293  fneqeql  5296  funimass3  5304  elrnrexdmb  5328  dff4im  5334  fconst4m  5402  elunirn  5426  riota1  5506  riota2df  5508  f1ocnvfv3  5521  eqfnov  5627  caoftrn  5756  mpt2xopovel  5879  rntpos  5895  ordgt0ge1  6041  iinerm  6201  erinxp  6203  qliftfun  6211  pr2nelem  6460  indpi  6532  genpdflem  6697  genpdisj  6713  genpassl  6714  genpassu  6715  ltnqpri  6784  ltpopr  6785  ltexprlemm  6790  ltexprlemdisj  6796  ltexprlemloc  6797  ltrennb  7022  letri3  7192  letr  7194  ltneg  7566  leneg  7569  reapltxor  7689  apsym  7706  suprnubex  8031  suprleubex  8032  elnnnn0  8331  zrevaddcl  8401  znnsub  8402  znn0sub  8416  prime  8446  eluz2  8625  eluz2b1  8688  nn01to3  8702  qrevaddcl  8729  xrletri3  8875  xrletr  8878  iccid  8948  elicopnf  8992  fzsplit2  9069  fzsn  9084  fzpr  9094  uzsplit  9109  fvinim0ffz  9250  lt2sqi  9563  le2sqi  9564  abs00ap  9948  gcddiv  10408  algcvgblem  10431  isprm3  10500  bj-sseq  10602