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  1434  sbal2  2071  eqsnm  3833  fnressn  5829  fressnfv  5830  eluniimadm  5895  iftrueb01  7419  genpassl  7722  genpassu  7723  1idprl  7788  1idpru  7789  axcaucvglemres  8097  negeq0  8411  muleqadd  8826  crap0  9116  addltmul  9359  fzrev  10292  modq0  10563  cjap0  11433  cjne0  11434  caucvgrelemrec  11505  lenegsq  11621  isumss  11917  fsumsplit  11933  sumsplitdc  11958  dvdsabseq  12373  pceu  12833  oddennn  12978  xpsfrnel  13392  metrest  15195  elabgf0  16196