Theorem bitr3di 194

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 131	. 2 |- ( th <-> ps )
3		bitr3di.1	. 2 |- ( ph -> ( ps <-> ch ) )
4	2, 3	syl5rbb 192	1 |- ( ph -> ( ch <-> th ) )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  xordc  1371  sbal2  1997  eqsnm  3714  fnressn  5646  fressnfv  5647  eluniimadm  5706  genpassl  7423  genpassu  7424  1idprl  7489  1idpru  7490  axcaucvglemres  7798  negeq0  8108  muleqadd  8521  crap0  8808  addltmul  9048  fzrev  9964  modq0  10206  cjap0  10784  cjne0  10785  caucvgrelemrec  10856  lenegsq  10972  isumss  11265  fsumsplit  11281  sumsplitdc  11306  dvdsabseq  11712  oddennn  12072  metrest  12845  elabgf0  13289