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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  xordc  1441  sbal2  2080  eqsnm  3880  fnressn  5904  fressnfv  5905  eluniimadm  5974  iftrueb01  7588  genpassl  7897  genpassu  7898  1idprl  7963  1idpru  7964  axcaucvglemres  8272  negeq0  8587  addeq0  8710  msqap0  9004  muleqadd  9006  crap0  9296  addltmul  9553  fzrev  10507  modq0  10786  cjap0  11694  cjne0  11695  caucvgrelemrec  11766  lenegsq  11883  isumss  12182  fsumsplit  12198  sumsplitdc  12223  dvdsabseq  12638  pceu  13102  oddennn  13340  xpsfrnel  13723  resscntz  14165  metrest  15749  elabgf0  17027