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  916  dn1dc  973  csbabg  3209  uniiunlem  3338  inimasn  5200  cnvpom  5325  fnresdisj  5488  f1oiso  6022  reldm  6410  mptelixpg  7006  1idprl  7947  1idpru  7948  nndiv  9324  fzn  10425  fz1sbc  10481  grpid  13821  znleval  14960  metrest  15530  loopclwwlkn1b  16574  clwwlknun  16596