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  3836  fnressn  5835  fressnfv  5836  eluniimadm  5901  iftrueb01  7431  genpassl  7734  genpassu  7735  1idprl  7800  1idpru  7801  axcaucvglemres  8109  negeq0  8423  muleqadd  8838  crap0  9128  addltmul  9371  fzrev  10309  modq0  10581  cjap0  11458  cjne0  11459  caucvgrelemrec  11530  lenegsq  11646  isumss  11942  fsumsplit  11958  sumsplitdc  11983  dvdsabseq  12398  pceu  12858  oddennn  13003  xpsfrnel  13417  metrest  15220  elabgf0  16309