Theorem bibi2d 232

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 180	. . . 4 |- ( ( ph -> ps ) <-> ( ph -> ch ) )
3	2	bibi2i 227	. . 3 |- ( ( ( ph -> th ) <-> ( ph -> ps ) ) <-> ( ( ph -> th ) <-> ( ph -> ch ) ) )
4		pm5.74 179	. . 3 |- ( ( ph -> ( th <-> ps ) ) <-> ( ( ph -> th ) <-> ( ph -> ps ) ) )
5		pm5.74 179	. . 3 |- ( ( ph -> ( th <-> ch ) ) <-> ( ( ph -> th ) <-> ( ph -> ch ) ) )
6	3, 4, 5	3bitr4i 212	. 2 |- ( ( ph -> ( th <-> ps ) ) <-> ( ph -> ( th <-> ch ) ) )
7	6	pm5.74ri 181	1 |- ( ph -> ( ( th <-> ps ) <-> ( th <-> ch ) ) )

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:  bibi1d  233  bibi12d  235  biantr  954  bimsc1  965  eujust  2047  euf  2050  ceqex  2891  reu6i  2955  axsep2  4152  zfauscl  4153  copsexg  4277  euotd  4287  cnveq0  5126  iotaval  5230  iota5  5240  eufnfv  5793  isoeq1  5848  isoeq3  5850  isores2  5860  isores3  5862  isotr  5863  isoini2  5866  riota5f  5902  caovordg  6091  caovord  6095  dfoprab4f  6251  frecabcl  6457  nnaword  6569  xpf1o  6905  ltanqg  7467  ltmnqg  7468  ltasrg  7837  axpre-ltadd  7953  prmdvdsexp  12316  subrgsubm  13790  bdsep2  15532  bdzfauscl  15536