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  1415  eubidh  2061  eubid  2062  axext3  2190  bm1.1  2192  eqeq1  2214  pm13.183  2918  elabgt  2921  elrab3t  2935  mob  2962  sbctt  3072  sbcabel  3088  isoeq2  5894  caovcang  6131  uchoice  6246  frecabcl  6508  expap0  10751  bezoutlemeu  12443  dfgcd3  12446  bezout  12447  prmdvdsexp  12585  ismet  14931  isxmet  14932  bdsepnft  16022  bdsepnfALT  16024