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  1403  sbal2  2039  eqsnm  3786  fnressn  5749  fressnfv  5750  eluniimadm  5813  genpassl  7593  genpassu  7594  1idprl  7659  1idpru  7660  axcaucvglemres  7968  negeq0  8282  muleqadd  8697  crap0  8987  addltmul  9230  fzrev  10161  modq0  10423  cjap0  11074  cjne0  11075  caucvgrelemrec  11146  lenegsq  11262  isumss  11558  fsumsplit  11574  sumsplitdc  11599  dvdsabseq  12014  pceu  12474  oddennn  12619  xpsfrnel  12997  metrest  14752  elabgf0  15433