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  5901  fressnfv  5902  eluniimadm  5971  iftrueb01  7582  genpassl  7891  genpassu  7892  1idprl  7957  1idpru  7958  axcaucvglemres  8266  negeq0  8581  addeq0  8704  msqap0  8998  muleqadd  9000  crap0  9290  addltmul  9546  fzrev  10501  modq0  10779  cjap0  11687  cjne0  11688  caucvgrelemrec  11759  lenegsq  11876  isumss  12174  fsumsplit  12190  sumsplitdc  12215  dvdsabseq  12630  pceu  13094  oddennn  13332  xpsfrnel  13714  metrest  15656  elabgf0  16903