Theorem syl6bbr 187

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 123	. 2 |- ( ch <-> th )
4	1, 3	syl6bb 185	1 |- ( ph -> ( ps <-> th ) )

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  3bitr4g  212  bibi2i  216  equsalh  1614  eueq3dc  2715  sbcel12g  2865  sbceqg  2866  sbcnel12g  2867  reldisj  3271  r19.3rm  3310  rabxp  4380  elrng  4526  iss  4654  eliniseg  4695  fcnvres  5073  dffv3g  5174  funimass4  5224  fndmdif  5272  fneqeql  5275  funimass3  5283  elrnrexdmb  5307  dff4im  5313  fconst4m  5381  elunirn  5405  riota1  5486  riota2df  5488  f1ocnvfv3  5501  eqfnov  5607  caoftrn  5736  mpt2xopovel  5856  rntpos  5872  ordgt0ge1  6018  iinerm  6178  erinxp  6180  qliftfun  6188  indpi  6440  genpdflem  6605  genpdisj  6621  genpassl  6622  genpassu  6623  ltnqpri  6692  ltpopr  6693  ltexprlemm  6698  ltexprlemdisj  6704  ltexprlemloc  6705  ltrennb  6930  letri3  7099  letr  7101  ltneg  7457  leneg  7460  reapltxor  7580  apsym  7597  elnnnn0  8225  zrevaddcl  8295  znnsub  8296  znn0sub  8309  prime  8337  eluz2  8479  eluz2b1  8539  nn01to3  8552  qrevaddcl  8578  xrletri3  8721  xrletr  8724  iccid  8794  elicopnf  8838  fzsplit2  8914  fzsn  8929  fzpr  8939  uzsplit  8954  fvinim0ffz  9096  lt2sqi  9341  le2sqi  9342  abs00ap  9660  algcvgblem  9888  bj-sseq  9931