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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  xordc  1441  sbal2  2080  eqsnm  3880  fnressn  5901  fressnfv  5902  eluniimadm  5971  iftrueb01  7583  genpassl  7892  genpassu  7893  1idprl  7958  1idpru  7959  axcaucvglemres  8267  negeq0  8582  addeq0  8705  msqap0  8999  muleqadd  9001  crap0  9291  addltmul  9547  fzrev  10502  modq0  10781  cjap0  11689  cjne0  11690  caucvgrelemrec  11761  lenegsq  11878  isumss  12177  fsumsplit  12193  sumsplitdc  12218  dvdsabseq  12633  pceu  13097  oddennn  13335  xpsfrnel  13718  resscntz  14160  metrest  15698  elabgf0  16971