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  2074  eqsnm  3859  fnressn  5870  fressnfv  5871  eluniimadm  5938  iftrueb01  7533  genpassl  7839  genpassu  7840  1idprl  7905  1idpru  7906  axcaucvglemres  8214  negeq0  8527  muleqadd  8942  crap0  9232  addltmul  9475  fzrev  10418  modq0  10691  cjap0  11592  cjne0  11593  caucvgrelemrec  11664  lenegsq  11780  isumss  12077  fsumsplit  12093  sumsplitdc  12118  dvdsabseq  12533  pceu  12993  oddennn  13143  xpsfrnel  13557  metrest  15371  elabgf0  16549