Theorem bibi1d 233

Description: Deduction adding a biconditional to the right in an equivalence. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
imbid.1	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
bibi1d	|- ( ph -> ( ( ps <-> th ) <-> ( ch <-> th ) ) )

Proof of Theorem bibi1d

Step	Hyp	Ref	Expression
1		imbid.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	bibi2d 232	. 2 |- ( ph -> ( ( th <-> ps ) <-> ( th <-> ch ) ) )
3		bicom 140	. 2 |- ( ( ps <-> th ) <-> ( th <-> ps ) )
4		bicom 140	. 2 |- ( ( ch <-> th ) <-> ( th <-> ch ) )
5	2, 3, 4	3bitr4g 223	1 |- ( ph -> ( ( ps <-> th ) <-> ( ch <-> th ) ) )

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:  bibi12d  235  bibi1  240  biassdc  1444  eubidh  2092  eubid  2093  axext3  2221  bm1.1  2223  eqeq1  2245  pm13.183  2964  elabgt  2967  elrab3t  2981  mob  3008  sbctt  3118  sbcabel  3134  isoeq2  6008  caovcang  6251  uchoice  6371  frecabcl  6670  expap0  11019  bezoutlemeu  12800  dfgcd3  12803  bezout  12804  prmdvdsexp  12943  ismet  15494  isxmet  15495  bdsepnft  17011  bdsepnfALT  17013