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  3757  fnressn  5704  fressnfv  5705  eluniimadm  5768  genpassl  7525  genpassu  7526  1idprl  7591  1idpru  7592  axcaucvglemres  7900  negeq0  8213  muleqadd  8627  crap0  8917  addltmul  9157  fzrev  10086  modq0  10331  cjap0  10918  cjne0  10919  caucvgrelemrec  10990  lenegsq  11106  isumss  11401  fsumsplit  11417  sumsplitdc  11442  dvdsabseq  11855  pceu  12297  oddennn  12395  xpsfrnel  12768  metrest  14045  elabgf0  14568