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  7582  genpassl  7891  genpassu  7892  1idprl  7957  1idpru  7958  axcaucvglemres  8266  negeq0  8580  addeq0  8703  msqap0  8996  muleqadd  8998  crap0  9288  addltmul  9542  fzrev  10491  modq0  10766  cjap0  11673  cjne0  11674  caucvgrelemrec  11745  lenegsq  11861  isumss  12158  fsumsplit  12174  sumsplitdc  12199  dvdsabseq  12614  pceu  13074  oddennn  13283  xpsfrnel  13665  metrest  15607  elabgf0  16805