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  1377  eubidh  2012  eubid  2013  axext3  2140  bm1.1  2142  eqeq1  2164  pm13.183  2850  elabgt  2853  elrab3t  2867  mob  2894  sbctt  3003  sbcabel  3018  isoeq2  5752  caovcang  5982  frecabcl  6346  expap0  10449  bezoutlemeu  11891  dfgcd3  11894  bezout  11895  prmdvdsexp  12023  ismet  12755  isxmet  12756  bdsepnft  13473  bdsepnfALT  13475