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 ) ) )

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:  bibi12d  235  bibi1  240  biassdc  1440  eubidh  2085  eubid  2086  axext3  2214  bm1.1  2216  eqeq1  2238  pm13.183  2945  elabgt  2948  elrab3t  2962  mob  2989  sbctt  3099  sbcabel  3115  isoeq2  5953  caovcang  6194  uchoice  6309  frecabcl  6608  expap0  10877  bezoutlemeu  12641  dfgcd3  12644  bezout  12645  prmdvdsexp  12783  ismet  15138  isxmet  15139  bdsepnft  16586  bdsepnfALT  16588