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  1437  sbal2  2073  eqsnm  3843  fnressn  5848  fressnfv  5849  eluniimadm  5916  iftrueb01  7484  genpassl  7787  genpassu  7788  1idprl  7853  1idpru  7854  axcaucvglemres  8162  negeq0  8475  muleqadd  8890  crap0  9180  addltmul  9423  fzrev  10364  modq0  10637  cjap0  11530  cjne0  11531  caucvgrelemrec  11602  lenegsq  11718  isumss  12015  fsumsplit  12031  sumsplitdc  12056  dvdsabseq  12471  pceu  12931  oddennn  13076  xpsfrnel  13490  metrest  15300  elabgf0  16478