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  1436  sbal2  2073  eqsnm  3838  fnressn  5840  fressnfv  5841  eluniimadm  5906  iftrueb01  7441  genpassl  7744  genpassu  7745  1idprl  7810  1idpru  7811  axcaucvglemres  8119  negeq0  8433  muleqadd  8848  crap0  9138  addltmul  9381  fzrev  10319  modq0  10592  cjap0  11485  cjne0  11486  caucvgrelemrec  11557  lenegsq  11673  isumss  11970  fsumsplit  11986  sumsplitdc  12011  dvdsabseq  12426  pceu  12886  oddennn  13031  xpsfrnel  13445  metrest  15249  elabgf0  16424