Theorem bitr2id 192

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

Hypotheses

Ref	Expression
bitr2id.1	|- ( ph <-> ps )
bitr2id.2	|- ( ch -> ( ps <-> th ) )

Assertion

Ref	Expression
bitr2id	|- ( ch -> ( th <-> ph ) )

Proof of Theorem bitr2id

Step	Hyp	Ref	Expression
1		bitr2id.1	. . 3 |- ( ph <-> ps )
2		bitr2id.2	. . 3 |- ( ch -> ( ps <-> th ) )
3	1, 2	syl5bb 191	. 2 |- ( ch -> ( ph <-> th ) )
4	3	bicomd 140	1 |- ( ch -> ( th <-> ph ) )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  bitr3di  194  pm5.17dc  894  dn1dc  949  csbabg  3101  uniiunlem  3226  inimasn  5015  cnvpom  5140  fnresdisj  5292  f1oiso  5788  reldm  6146  mptelixpg  6691  1idprl  7522  1idpru  7523  nndiv  8889  fzn  9967  fz1sbc  10021  metrest  13047