Theorem bitr2id 193

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	bitrid 192	. 2 |- ( ch -> ( ph <-> th ) )
4	3	bicomd 141	1 |- ( ch -> ( th <-> ph ) )

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  bitr3di  195  pm5.17dc  912  dn1dc  969  csbabg  3200  uniiunlem  3328  inimasn  5180  cnvpom  5305  fnresdisj  5468  f1oiso  5999  reldm  6380  mptelixpg  6969  1idprl  7905  1idpru  7906  nndiv  9278  fzn  10376  fz1sbc  10430  grpid  13752  znleval  14801  metrest  15371  loopclwwlkn1b  16414  clwwlknun  16436