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  3832  fnressn  5824  fressnfv  5825  eluniimadm  5888  iftrueb01  7404  genpassl  7707  genpassu  7708  1idprl  7773  1idpru  7774  axcaucvglemres  8082  negeq0  8396  muleqadd  8811  crap0  9101  addltmul  9344  fzrev  10276  modq0  10546  cjap0  11413  cjne0  11414  caucvgrelemrec  11485  lenegsq  11601  isumss  11897  fsumsplit  11913  sumsplitdc  11938  dvdsabseq  12353  pceu  12813  oddennn  12958  xpsfrnel  13372  metrest  15174  elabgf0  16099