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  1998  eqsnm  3690  fnressn  5614  fressnfv  5615  eluniimadm  5674  genpassl  7356  genpassu  7357  1idprl  7422  1idpru  7423  axcaucvglemres  7731  negeq0  8040  muleqadd  8453  crap0  8740  addltmul  8980  fzrev  9895  modq0  10133  cjap0  10711  cjne0  10712  caucvgrelemrec  10783  lenegsq  10899  isumss  11192  fsumsplit  11208  sumsplitdc  11233  dvdsabseq  11581  oddennn  11941  metrest  12714  elabgf0  13155