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  1392  sbal2  2020  eqsnm  3756  fnressn  5703  fressnfv  5704  eluniimadm  5766  genpassl  7523  genpassu  7524  1idprl  7589  1idpru  7590  axcaucvglemres  7898  negeq0  8211  muleqadd  8625  crap0  8915  addltmul  9155  fzrev  10084  modq0  10329  cjap0  10916  cjne0  10917  caucvgrelemrec  10988  lenegsq  11104  isumss  11399  fsumsplit  11415  sumsplitdc  11440  dvdsabseq  11853  pceu  12295  oddennn  12393  xpsfrnel  12763  metrest  14009  elabgf0  14532