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  911  dn1dc  968  csbabg  3189  uniiunlem  3316  inimasn  5154  cnvpom  5279  fnresdisj  5442  f1oiso  5966  reldm  6348  mptelixpg  6902  1idprl  7809  1idpru  7810  nndiv  9183  fzn  10276  fz1sbc  10330  grpid  13621  znleval  14666  metrest  15229  loopclwwlkn1b  16269  clwwlknun  16291