Theorem bibi2d 230

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 178	. . . 4 |- ( ( ph -> ps ) <-> ( ph -> ch ) )
3	2	bibi2i 225	. . 3 |- ( ( ( ph -> th ) <-> ( ph -> ps ) ) <-> ( ( ph -> th ) <-> ( ph -> ch ) ) )
4		pm5.74 177	. . 3 |- ( ( ph -> ( th <-> ps ) ) <-> ( ( ph -> th ) <-> ( ph -> ps ) ) )
5		pm5.74 177	. . 3 |- ( ( ph -> ( th <-> ch ) ) <-> ( ( ph -> th ) <-> ( ph -> ch ) ) )
6	3, 4, 5	3bitr4i 210	. 2 |- ( ( ph -> ( th <-> ps ) ) <-> ( ph -> ( th <-> ch ) ) )
7	6	pm5.74ri 179	1 |- ( ph -> ( ( th <-> ps ) <-> ( th <-> ch ) ) )

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  bibi1d  231  bibi12d  233  biantr  893  bimsc1  904  eujust  1943  euf  1946  ceqex  2722  reu6i  2783  axsep2  3897  zfauscl  3898  copsexg  3999  euotd  4009  cnveq0  4797  iotaval  4898  iota5  4907  eufnfv  5410  isoeq1  5461  isoeq3  5463  isores2  5473  isores3  5475  isotr  5476  isoini2  5478  riota5f  5512  caovordg  5688  caovord  5692  dfoprab4f  5839  nnaword  6107  ltanqg  6590  ltmnqg  6591  ltasrg  6947  axpre-ltadd  7052  prmdvdsexp  10527  bdsep2  10677  bdzfauscl  10681  strcoll2  10778  sscoll2  10783