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  6011  caovcang  6254  uchoice  6375  frecabcl  6675  expap0  11026  bezoutlemeu  12808  dfgcd3  12811  bezout  12812  prmdvdsexp  12951  ismet  15587  isxmet  15588  bdsepnft  17135  bdsepnfALT  17137