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  1412  sbal2  2049  eqsnm  3802  fnressn  5783  fressnfv  5784  eluniimadm  5847  iftrueb01  7354  genpassl  7657  genpassu  7658  1idprl  7723  1idpru  7724  axcaucvglemres  8032  negeq0  8346  muleqadd  8761  crap0  9051  addltmul  9294  fzrev  10226  modq0  10496  cjap0  11293  cjne0  11294  caucvgrelemrec  11365  lenegsq  11481  isumss  11777  fsumsplit  11793  sumsplitdc  11818  dvdsabseq  12233  pceu  12693  oddennn  12838  xpsfrnel  13251  metrest  15053  elabgf0  15852