Theorem bibi1d 471

Description: Deduction adding a biconditional to the right in an equivalence.

Hypothesis

Ref	Expression
bid.1	|- (ph -> (ps <-> ch))

Assertion

Ref	Expression
bibi1d	|- (ph -> ((ps <-> th) <-> (ch <-> th)))

Proof of Theorem bibi1d

Step	Hyp	Ref	Expression
1		bid.1	. . 3 |- (ph -> (ps <-> ch))
2	1	bibi2d 470	. 2 |- (ph -> ((th <-> ps) <-> (th <-> ch)))
3		bicom 398	. 2 |- ((ps <-> th) <-> (th <-> ps))
4		bicom 398	. 2 |- ((ch <-> th) <-> (th <-> ch))
5	2, 3, 4	3bitr4g 428	1 |- (ph -> ((ps <-> th) <-> (ch <-> th)))

Syntax hints:   -> wi 2   <-> wb 127

This theorem is referenced by:  bibi12d 477  bieud 1012  zfext2 1087  bm1.1 1088  cleq1 1107  axrep 1473  isoeq2 2926  axacndlem4 3756  axacnd 3758  addcant 4122  mulcant 4208  mulcant2 4209  lesub0t 4374

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

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org