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  1437  sbal2  2076  eqsnm  3864  fnressn  5875  fressnfv  5876  eluniimadm  5944  iftrueb01  7546  genpassl  7855  genpassu  7856  1idprl  7921  1idpru  7922  axcaucvglemres  8230  negeq0  8543  addeq0  8666  muleqadd  8959  crap0  9249  addltmul  9492  fzrev  10440  modq0  10715  cjap0  11617  cjne0  11618  caucvgrelemrec  11689  lenegsq  11805  isumss  12102  fsumsplit  12118  sumsplitdc  12143  dvdsabseq  12558  pceu  13018  oddennn  13227  xpsfrnel  13608  metrest  15497  elabgf0  16675