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  10508  modq0  10787  cjap0  11695  cjne0  11696  caucvgrelemrec  11767  lenegsq  11884  isumss  12183  fsumsplit  12199  sumsplitdc  12224  dvdsabseq  12639  pceu  13103  oddennn  13341  xpsfrnel  13724  resscntz  14166  metrest  15732  elabgf0  17010