Theorem syl6bbr 254

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  3bitr4g  279  bibi2i  304  mtt  329  nbn2  334  equsalhwOLD  1839  equsal  1960  necon2abid  2574  eueq3  3012  sbcabel  3124  sbcel12g  3152  sbceqg  3153  sbcnel12g  3154  sbcne12g  3155  n0moeu  3563  reldisj  3595  r19.3rz  3642  r19.3rzv  3644  r19.9rzv  3645  pw1in  4165  opkelimagekg  4272  eqpw1uni  4331  addcid1  4406  eqtfinrelk  4487  nnadjoin  4521  proj1op  4601  phidisjnn  4616  phialllem1  4617  rabxp  4815  brswap2  4861  iss  5001  xpcan  5058  xpcan2  5059  dffn5  5364  fnrnfv  5365  funimass4  5369  funimass3  5405  inpreima  5410  fnasrn  5418  dff4  5422  fconst4  5459  f1ofveu  5481  eqfnov  5590  txpcofun  5804  mapsn  6027  elncs  6120  ce0addcnnul  6180  ce0nnulb  6183  ceclb  6184  sbth  6207  lectr  6212  nchoicelem8  6297  nchoicelem12  6301  nchoicelem16  6305  fnfreclem3  6320