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  1385  eubidh  2020  eubid  2021  axext3  2148  bm1.1  2150  eqeq1  2172  pm13.183  2864  elabgt  2867  elrab3t  2881  mob  2908  sbctt  3017  sbcabel  3032  isoeq2  5770  caovcang  6003  frecabcl  6367  expap0  10485  bezoutlemeu  11940  dfgcd3  11943  bezout  11944  prmdvdsexp  12080  ismet  12984  isxmet  12985  bdsepnft  13769  bdsepnfALT  13771