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  1661  eueq3dc  2789  sbcel12g  2946  sbceqg  2947  sbcnel12g  2948  reldisj  3334  r19.3rm  3370  rabxp  4474  elrng  4627  iss  4758  eliniseg  4802  fcnvres  5194  dffv3g  5301  funimass4  5355  fndmdif  5404  fneqeql  5407  funimass3  5415  elrnrexdmb  5439  dff4im  5445  fconst4m  5517  elunirn  5545  riota1  5626  riota2df  5628  f1ocnvfv3  5641  eqfnov  5751  caoftrn  5880  mpt2xopovel  6006  rntpos  6022  ordgt0ge1  6199  iinerm  6362  erinxp  6364  qliftfun  6372  mapdm0  6418  isomnimap  6791  pr2nelem  6817  indpi  6899  genpdflem  7064  genpdisj  7080  genpassl  7081  genpassu  7082  ltnqpri  7151  ltpopr  7152  ltexprlemm  7157  ltexprlemdisj  7163  ltexprlemloc  7164  ltrennb  7389  letri3  7564  letr  7566  ltneg  7938  leneg  7941  reapltxor  8064  apsym  8081  suprnubex  8412  suprleubex  8413  elnnnn0  8714  zrevaddcl  8798  znnsub  8799  znn0sub  8813  prime  8843  eluz2  9023  eluz2b1  9086  nn01to3  9100  qrevaddcl  9127  xrletri3  9268  xrletr  9271  iccid  9341  elicopnf  9385  fzsplit2  9462  fzsn  9477  fzpr  9487  uzsplit  9502  fvinim0ffz  9648  lt2sqi  10038  le2sqi  10039  abs00ap  10491  mertenslem2  10926  gcddiv  11282  algcvgblem  11305  isprm3  11374  bj-sseq  11647  nnti  11847