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  1390  eubidh  2025  eubid  2026  axext3  2153  bm1.1  2155  eqeq1  2177  pm13.183  2868  elabgt  2871  elrab3t  2885  mob  2912  sbctt  3021  sbcabel  3036  isoeq2  5781  caovcang  6014  frecabcl  6378  expap0  10506  bezoutlemeu  11962  dfgcd3  11965  bezout  11966  prmdvdsexp  12102  ismet  13138  isxmet  13139  bdsepnft  13922  bdsepnfALT  13924