Theorem bibi2d 309

Description: Deduction adding a biconditional to the left in an equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 19-May-2013.)

Hypothesis

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

Assertion

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

Proof of Theorem bibi2d

Step	Hyp	Ref	Expression
1		imbid.1	. . . . 5 |- (ph -> (ps <-> ch))
2	1	pm5.74i 236	. . . 4 |- ((ph -> ps) <-> (ph -> ch))
3	2	bibi2i 304	. . 3 |- (((ph -> th) <-> (ph -> ps)) <-> ((ph -> th) <-> (ph -> ch)))
4		pm5.74 235	. . 3 |- ((ph -> (th <-> ps)) <-> ((ph -> th) <-> (ph -> ps)))
5		pm5.74 235	. . 3 |- ((ph -> (th <-> ch)) <-> ((ph -> th) <-> (ph -> ch)))
6	3, 4, 5	3bitr4i 268	. 2 |- ((ph -> (th <-> ps)) <-> (ph -> (th <-> ch)))
7	6	pm5.74ri 237	1 |- (ph -> ((th <-> ps) <-> (th <-> ch)))

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

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

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  bibi1d  310  bibi12d  312  biantr  897  bimsc1  904  eujust  2206  eujustALT  2207  euf  2210  ceqex  2969  reu6i  3027  sbc2or  3054  iotaval  4350  iota5  4359  copsexg  4607  isoeq1  5482  isoeq3  5484  isores2  5493  isoini2  5498  caovord  5629  extd  5923