Theorem bitr3di 195

Description: A syllogism inference from two biconditionals. (Contributed by NM, 25-Nov-1994.)

Hypotheses

Ref	Expression
bitr3di.1	|- ( ph -> ( ps <-> ch ) )
bitr3di.2	|- ( ps <-> th )

Assertion

Ref	Expression
bitr3di	|- ( ph -> ( ch <-> th ) )

Proof of Theorem bitr3di

Step	Hyp	Ref	Expression
1		bitr3di.2	. . 3 |- ( ps <-> th )
2	1	bicomi 132	. 2 |- ( th <-> ps )
3		bitr3di.1	. 2 |- ( ph -> ( ps <-> ch ) )
4	2, 3	bitr2id 193	1 |- ( ph -> ( ch <-> th ) )

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:  xordc  1403  sbal2  2032  eqsnm  3770  fnressn  5723  fressnfv  5724  eluniimadm  5787  genpassl  7553  genpassu  7554  1idprl  7619  1idpru  7620  axcaucvglemres  7928  negeq0  8241  muleqadd  8655  crap0  8945  addltmul  9185  fzrev  10114  modq0  10360  cjap0  10948  cjne0  10949  caucvgrelemrec  11020  lenegsq  11136  isumss  11431  fsumsplit  11447  sumsplitdc  11472  dvdsabseq  11885  pceu  12327  oddennn  12443  xpsfrnel  12820  metrest  14463  elabgf0  14987