Theorem bibi1d 231

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 230	. 2 |- ( ph -> ( ( th <-> ps ) <-> ( th <-> ch ) ) )
3		bicom 138	. 2 |- ( ( ps <-> th ) <-> ( th <-> ps ) )
4		bicom 138	. 2 |- ( ( ch <-> th ) <-> ( th <-> ch ) )
5	2, 3, 4	3bitr4g 221	1 |- ( ph -> ( ( ps <-> th ) <-> ( ch <-> th ) ) )

Syntax hints:   -> wi 4   <-> wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  bibi12d  233  bibi1  238  biassdc  1326  eubidh  1947  eubid  1948  axext3  2064  bm1.1  2066  eqeq1  2087  pm13.183  2732  elabgt  2735  elrab3t  2748  mob  2774  sbctt  2880  sbcabel  2895  isoeq2  5462  caovcang  5682  expap0  9506  bezoutlemeu  10396  dfgcd3  10399  bezout  10400  prmdvdsexp  10527  bdsepnft  10678  bdsepnfALT  10680  strcollnft  10779  strcollnfALT  10781