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  958  bimsc1  969  eujust  2079  euf  2082  ceqex  2930  reu6i  2994  axsep2  4202  zfauscl  4203  copsexg  4329  euotd  4340  cnveq0  5184  iotaval  5289  iota5  5299  eufnfv  5869  isoeq1  5924  isoeq3  5926  isores2  5936  isores3  5938  isotr  5939  isoini2  5942  riota5f  5980  caovordg  6172  caovord  6176  dfoprab4f  6337  frecabcl  6543  nnaword  6655  xpf1o  7001  ltanqg  7583  ltmnqg  7584  ltasrg  7953  axpre-ltadd  8069  prmdvdsexp  12665  subrgsubm  14192  bdsep2  16207  bdzfauscl  16211