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  5751  fressnfv  5752  eluniimadm  5815  genpassl  7608  genpassu  7609  1idprl  7674  1idpru  7675  axcaucvglemres  7983  negeq0  8297  muleqadd  8712  crap0  9002  addltmul  9245  fzrev  10176  modq0  10438  cjap0  11089  cjne0  11090  caucvgrelemrec  11161  lenegsq  11277  isumss  11573  fsumsplit  11589  sumsplitdc  11614  dvdsabseq  12029  pceu  12489  oddennn  12634  xpsfrnel  13046  metrest  14826  elabgf0  15507