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  3754  fnressn  5699  fressnfv  5700  eluniimadm  5761  genpassl  7518  genpassu  7519  1idprl  7584  1idpru  7585  axcaucvglemres  7893  negeq0  8205  muleqadd  8619  crap0  8909  addltmul  9149  fzrev  10077  modq0  10322  cjap0  10907  cjne0  10908  caucvgrelemrec  10979  lenegsq  11095  isumss  11390  fsumsplit  11406  sumsplitdc  11431  dvdsabseq  11843  pceu  12285  oddennn  12383  metrest  13788  elabgf0  14300