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-mp 5  ax-1 6  ax-2 7  ax-3 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  2970  reu6i  3028  sbc2or  3055  iotaval  4351  iota5  4360  copsexg  4608  isoeq1  5483  isoeq3  5485  isores2  5494  isoini2  5499  caovord  5630  extd  5924