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  2039  eqsnm  3785  fnressn  5748  fressnfv  5749  eluniimadm  5812  genpassl  7591  genpassu  7592  1idprl  7657  1idpru  7658  axcaucvglemres  7966  negeq0  8280  muleqadd  8695  crap0  8985  addltmul  9228  fzrev  10159  modq0  10421  cjap0  11072  cjne0  11073  caucvgrelemrec  11144  lenegsq  11260  isumss  11556  fsumsplit  11572  sumsplitdc  11597  dvdsabseq  12012  pceu  12464  oddennn  12609  xpsfrnel  12987  metrest  14742  elabgf0  15423