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  2076  eqsnm  3861  fnressn  5872  fressnfv  5873  eluniimadm  5940  iftrueb01  7535  genpassl  7841  genpassu  7842  1idprl  7907  1idpru  7908  axcaucvglemres  8216  negeq0  8529  muleqadd  8944  crap0  9234  addltmul  9477  fzrev  10422  modq0  10695  cjap0  11596  cjne0  11597  caucvgrelemrec  11668  lenegsq  11784  isumss  12081  fsumsplit  12097  sumsplitdc  12122  dvdsabseq  12537  pceu  12997  oddennn  13160  xpsfrnel  13574  metrest  15388  elabgf0  16566