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  1441  sbal2  2080  eqsnm  3875  fnressn  5892  fressnfv  5893  eluniimadm  5961  iftrueb01  7572  genpassl  7881  genpassu  7882  1idprl  7947  1idpru  7948  axcaucvglemres  8256  negeq0  8570  addeq0  8693  msqap0  8986  muleqadd  8988  crap0  9278  addltmul  9521  fzrev  10469  modq0  10744  cjap0  11651  cjne0  11652  caucvgrelemrec  11723  lenegsq  11839  isumss  12136  fsumsplit  12152  sumsplitdc  12177  dvdsabseq  12592  pceu  13052  oddennn  13261  xpsfrnel  13642  metrest  15530  elabgf0  16719