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

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:  bitr4id  199  bibif  703  pm5.61  799  oranabs  820  pm5.7dc  960  nbbndc  1436  resopab2  5052  xpcom  5275  f1od2  6387  map1  6973  ac6sfi  7068  elznn0  9472  rexuz3  11516  xrmaxiflemcom  11775  metrest  15195  sincosq3sgn  15517  sincosq4sgn  15518  lgsquadlem3  15773  pw1map  16420