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  3203  uniiunlem  3332  inimasn  5185  cnvpom  5310  fnresdisj  5473  f1oiso  6005  reldm  6393  mptelixpg  6982  1idprl  7921  1idpru  7922  nndiv  9295  fzn  10396  fz1sbc  10452  grpid  13794  znleval  14927  metrest  15497  loopclwwlkn1b  16540  clwwlknun  16562