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  1331  eubidh  1954  eubid  1955  axext3  2071  bm1.1  2073  eqeq1  2094  pm13.183  2754  elabgt  2757  elrab3t  2770  mob  2797  sbctt  2905  sbcabel  2920  isoeq2  5581  caovcang  5806  frecabcl  6164  expap0  9981  bezoutlemeu  11270  dfgcd3  11273  bezout  11274  prmdvdsexp  11401  bdsepnft  11733  bdsepnfALT  11735  strcollnft  11834  strcollnfALT  11836