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  961  bimsc1  972  eujust  2082  euf  2085  ceqex  2944  reu6i  3008  axsep2  4229  zfauscl  4230  copsexg  4360  euotd  4371  cnveq0  5219  iotaval  5324  iota5  5334  eufnfv  5917  isoeq1  5974  isoeq3  5976  isores2  5986  isores3  5988  isotr  5989  isoini2  5992  riota5f  6030  caovordg  6222  caovord  6226  dfoprab4f  6387  frecabcl  6630  nnaword  6744  xpf1o  7097  ltanqg  7715  ltmnqg  7716  ltasrg  8085  axpre-ltadd  8201  prmdvdsexp  12845  subrgsubm  14379  wlkeq  16349  bdsep2  16656  bdzfauscl  16660