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 ) ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  bibi1d  233  bibi12d  235  biantr  965  bimsc1  976  eujust  2088  euf  2091  ceqex  2953  reu6i  3017  axsepg  4252  sepg  4253  zfausclOLD  4255  copsexg  4386  euotd  4397  cnveq0  5247  iotaval  5352  iota5  5362  eufnfv  5952  isoeq1  6010  isoeq3  6012  isores2  6022  isores3  6024  isotr  6025  isoini2  6028  riota5f  6068  caovordg  6260  caovord  6264  dfoprab4f  6431  frecabcl  6674  nnaword  6788  xpf1o  7148  ltanqg  7773  ltmnqg  7774  ltasrg  8143  axpre-ltadd  8259  prmdvdsexp  12952  subrgsubm  14651  wlkeq  16800  bdsep2  17117  bdsepg  17121  stnot  17244