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  1406  eubidh  2051  eubid  2052  axext3  2179  bm1.1  2181  eqeq1  2203  pm13.183  2902  elabgt  2905  elrab3t  2919  mob  2946  sbctt  3056  sbcabel  3071  isoeq2  5849  caovcang  6085  uchoice  6195  frecabcl  6457  expap0  10661  bezoutlemeu  12174  dfgcd3  12177  bezout  12178  prmdvdsexp  12316  ismet  14580  isxmet  14581  bdsepnft  15533  bdsepnfALT  15535