Theorem syl6bbr 254

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

Hypotheses

Ref	Expression
syl6bbr.1	⊢ (φ → (ψ ↔ χ))
syl6bbr.2	⊢ (θ ↔ χ)

Assertion

Ref	Expression
syl6bbr	⊢ (φ → (ψ ↔ θ))

Proof of Theorem syl6bbr

Step	Hyp	Ref	Expression
1		syl6bbr.1	. 2 ⊢ (φ → (ψ ↔ χ))
2		syl6bbr.2	. . 3 ⊢ (θ ↔ χ)
3	2	bicomi 193	. 2 ⊢ (χ ↔ θ)
4	1, 3	syl6bb 252	1 ⊢ (φ → (ψ ↔ θ))

Syntax hints:   → wi 4   ↔ wb 176

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 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  2573  eueq3  3011  sbcabel  3123  sbcel12g  3151  sbceqg  3152  sbcnel12g  3153  sbcne12g  3154  n0moeu  3562  reldisj  3594  r19.3rz  3641  r19.3rzv  3643  r19.9rzv  3644  pw1in  4164  opkelimagekg  4271  eqpw1uni  4330  addcid1  4405  eqtfinrelk  4486  nnadjoin  4520  proj1op  4600  phidisjnn  4615  phialllem1  4616  rabxp  4814  brswap2  4860  iss  5000  xpcan  5057  xpcan2  5058  dffn5  5363  fnrnfv  5364  funimass4  5368  funimass3  5404  inpreima  5409  fnasrn  5417  dff4  5421  fconst4  5458  f1ofveu  5480  eqfnov  5589  txpcofun  5803  mapsn  6026  elncs  6119  ce0addcnnul  6179  ce0nnulb  6182  ceclb  6183  sbth  6206  lectr  6211  nchoicelem8  6296  nchoicelem12  6300  nchoicelem16  6304  fnfreclem3  6319