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  1436  sbal2  2073  eqsnm  3838  fnressn  5839  fressnfv  5840  eluniimadm  5905  iftrueb01  7440  genpassl  7743  genpassu  7744  1idprl  7809  1idpru  7810  axcaucvglemres  8118  negeq0  8432  muleqadd  8847  crap0  9137  addltmul  9380  fzrev  10318  modq0  10590  cjap0  11467  cjne0  11468  caucvgrelemrec  11539  lenegsq  11655  isumss  11951  fsumsplit  11967  sumsplitdc  11992  dvdsabseq  12407  pceu  12867  oddennn  13012  xpsfrnel  13426  metrest  15229  elabgf0  16373