Theorem bibi1d 232

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 231	. 2 |- ( ph -> ( ( th <-> ps ) <-> ( th <-> ch ) ) )
3		bicom 139	. 2 |- ( ( ps <-> th ) <-> ( th <-> ps ) )
4		bicom 139	. 2 |- ( ( ch <-> th ) <-> ( th <-> ch ) )
5	2, 3, 4	3bitr4g 222	1 |- ( ph -> ( ( ps <-> th ) <-> ( ch <-> th ) ) )

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  bibi12d  234  bibi1  239  biassdc  1374  eubidh  2006  eubid  2007  axext3  2123  bm1.1  2125  eqeq1  2147  pm13.183  2826  elabgt  2829  elrab3t  2843  mob  2870  sbctt  2979  sbcabel  2994  isoeq2  5711  caovcang  5940  frecabcl  6304  expap0  10354  bezoutlemeu  11731  dfgcd3  11734  bezout  11735  prmdvdsexp  11862  ismet  12552  isxmet  12553  bdsepnft  13256  bdsepnfALT  13258