Theorem bitr2di 197

Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
bitr2di.1	|- ( ph -> ( ps <-> ch ) )
bitr2di.2	|- ( ch <-> th )

Assertion

Ref	Expression
bitr2di	|- ( ph -> ( th <-> ps ) )

Proof of Theorem bitr2di

Step	Hyp	Ref	Expression
1		bitr2di.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2		bitr2di.2	. . 3 |- ( ch <-> th )
3	1, 2	bitrdi 196	. 2 |- ( ph -> ( ps <-> th ) )
4	3	bicomd 141	1 |- ( ph -> ( th <-> ps ) )

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:  bitr4id  199  bibif  710  pm5.61  806  oranabs  827  pm5.7dc  967  nbbndc  1443  resopab2  5113  xpcom  5337  f1od2  6475  map1  7105  ac6sfi  7206  elznn0  9670  rexuz3  11778  xrmaxiflemcom  12040  metrest  15732  sincosq3sgn  16055  sincosq4sgn  16056  lgsquadlem3  16403  pw1map  17230