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  955  bimsc1  966  eujust  2057  euf  2060  ceqex  2904  reu6i  2968  axsep2  4174  zfauscl  4175  copsexg  4301  euotd  4312  cnveq0  5153  iotaval  5257  iota5  5267  eufnfv  5833  isoeq1  5888  isoeq3  5890  isores2  5900  isores3  5902  isotr  5903  isoini2  5906  riota5f  5942  caovordg  6132  caovord  6136  dfoprab4f  6297  frecabcl  6503  nnaword  6615  xpf1o  6961  ltanqg  7543  ltmnqg  7544  ltasrg  7913  axpre-ltadd  8029  prmdvdsexp  12555  subrgsubm  14081  bdsep2  15991  bdzfauscl  15995