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  1611  eueq3dc  2709  sbcel12g  2859  sbceqg  2860  sbcnel12g  2861  reldisj  3265  r19.3rm  3304  rabxp  4323  elrng  4469  iss  4597  eliniseg  4638  fcnvres  5016  dffv3g  5117  funimass4  5167  fndmdif  5215  fneqeql  5218  funimass3  5226  elrnrexdmb  5250  dff4im  5256  fconst4m  5324  elunirn  5348  riota1  5429  riota2df  5431  f1ocnvfv3  5444  eqfnov  5549  caoftrn  5678  mpt2xopovel  5797  rntpos  5813  ordgt0ge1  5957  iinerm  6114  erinxp  6116  qliftfun  6124  indpi  6326  genpdflem  6490  genpdisj  6506  genpassl  6507  genpassu  6508  ltpopr  6569  ltexprlemm  6574  ltexprlemdisj  6580  ltexprlemloc  6581  letri3  6896  letr  6898  ltneg  7252  leneg  7255  reapltxor  7373  apsym  7390  elnnnn0  8001  zrevaddcl  8071  znnsub  8072  znn0sub  8085  prime  8113  eluz2  8255  eluz2b1  8315  nn01to3  8328  qrevaddcl  8353  xrletri3  8491  xrletr  8494  iccid  8564  elicopnf  8608  fzsplit2  8684  fzsn  8699  fzpr  8709  uzsplit  8724  lt2sqi  8994  le2sqi  8995  bj-sseq  9266