Theorem bitr3 342

Description: Closed nested implication form of bitr3i 266. Derived automatically from bitr3VD 39084. (Contributed by Alan Sare, 31-Dec-2011.)

Assertion

Ref	Expression
bitr3	|- ( ( ph <-> ps ) -> ( ( ph <-> ch ) -> ( ps <-> ch ) ) )

Proof of Theorem bitr3

Step	Hyp	Ref	Expression
1		bibi1 341	. 2 |- ( ( ph <-> ps ) -> ( ( ph <-> ch ) <-> ( ps <-> ch ) ) )
2	1	biimpd 219	1 |- ( ( ph <-> ps ) -> ( ( ph <-> ch ) -> ( ps <-> ch ) ) )

Syntax hints:   -> wi 4   <-> wb 196

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197

This theorem is referenced by:  sumodd  15111  3orbi123VD  39085  sbc3orgVD  39086  trsbcVD  39113  csbrngVD  39132  e2ebindVD  39148  e2ebindALT  39165