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  4250  sepg  4251  zfausclOLD  4253  copsexg  4384  euotd  4395  cnveq0  5244  iotaval  5349  iota5  5359  eufnfv  5949  isoeq1  6007  isoeq3  6009  isores2  6019  isores3  6021  isotr  6022  isoini2  6025  riota5f  6065  caovordg  6257  caovord  6261  dfoprab4f  6427  frecabcl  6670  nnaword  6784  xpf1o  7144  ltanqg  7768  ltmnqg  7769  ltasrg  8138  axpre-ltadd  8254  prmdvdsexp  12946  subrgsubm  14626  wlkeq  16761  bdsep2  17078  bdsepg  17082  stnot  17205