Theorem bibi2d 231

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 179	. . . 4 |- ( ( ph -> ps ) <-> ( ph -> ch ) )
3	2	bibi2i 226	. . 3 |- ( ( ( ph -> th ) <-> ( ph -> ps ) ) <-> ( ( ph -> th ) <-> ( ph -> ch ) ) )
4		pm5.74 178	. . 3 |- ( ( ph -> ( th <-> ps ) ) <-> ( ( ph -> th ) <-> ( ph -> ps ) ) )
5		pm5.74 178	. . 3 |- ( ( ph -> ( th <-> ch ) ) <-> ( ( ph -> th ) <-> ( ph -> ch ) ) )
6	3, 4, 5	3bitr4i 211	. 2 |- ( ( ph -> ( th <-> ps ) ) <-> ( ph -> ( th <-> ch ) ) )
7	6	pm5.74ri 180	1 |- ( ph -> ( ( th <-> ps ) <-> ( th <-> ch ) ) )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  bibi1d  232  bibi12d  234  biantr  904  bimsc1  915  eujust  1962  euf  1965  ceqex  2766  reu6i  2828  axsep2  3987  zfauscl  3988  copsexg  4104  euotd  4114  cnveq0  4931  iotaval  5035  iota5  5044  eufnfv  5580  isoeq1  5634  isoeq3  5636  isores2  5646  isores3  5648  isotr  5649  isoini2  5652  riota5f  5686  caovordg  5870  caovord  5874  dfoprab4f  6021  frecabcl  6226  nnaword  6337  xpf1o  6667  ltanqg  7109  ltmnqg  7110  ltasrg  7466  axpre-ltadd  7571  prmdvdsexp  11619  bdsep2  12665  bdzfauscl  12669  strcoll2  12766  sscoll2  12771