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  909  dn1dc  966  csbabg  3187  uniiunlem  3314  inimasn  5152  cnvpom  5277  fnresdisj  5439  f1oiso  5962  reldm  6344  mptelixpg  6898  1idprl  7800  1idpru  7801  nndiv  9174  fzn  10267  fz1sbc  10321  grpid  13612  znleval  14657  metrest  15220  loopclwwlkn1b  16214  clwwlknun  16236