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  1373  eubidh  2005  eubid  2006  axext3  2122  bm1.1  2124  eqeq1  2146  pm13.183  2822  elabgt  2825  elrab3t  2839  mob  2866  sbctt  2975  sbcabel  2990  isoeq2  5703  caovcang  5932  frecabcl  6296  expap0  10323  bezoutlemeu  11695  dfgcd3  11698  bezout  11699  prmdvdsexp  11826  ismet  12513  isxmet  12514  bdsepnft  13085  bdsepnfALT  13087  strcollnft  13182  strcollnfALT  13184