Theorem bibi1d 325

Description: Deduction adding a biconditional to the right in an equivalence. (Contributed by NM, 11-May-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 324	. 2 |- ( ph -> ( ( th <-> ps ) <-> ( th <-> ch ) ) )
3		bicom 205	. 2 |- ( ( ps <-> th ) <-> ( th <-> ps ) )
4		bicom 205	. 2 |- ( ( ch <-> th ) <-> ( th <-> ch ) )
5	2, 3, 4	3bitr4g 296	1 |- ( ph -> ( ( ps <-> th ) <-> ( ch <-> th ) ) )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 190

This theorem is referenced by:  bibi12d  327  bibi1  333  biass  365  eubid  2327  axext3  2443  axext3ALT  2444  bm1.1  2446  eqeq1dALT  2464  pm13.183  3190  elabgt  3193  elrab3t  3206  mob  3231  sbctt  3341  sbcabel  3356  isoeq2  6235  caovcang  6496  domunfican  7869  axacndlem4  9060  axacnd  9062  expeq0  12333  dfrtrclrec2  13168  relexpind  13175  prmdvdsexp  14715  isacs  15605  acsfn  15613  tsrlemax  16514  odeq  17247  isslw  17308  isabv  18095  t0sep  20388  xkopt  20718  kqt0lem  20799  r0sep  20811  nrmr0reg  20812  ismet  21386  isxmet  21387  stdbdxmet  21578  xrsxmet  21875  iccpnfcnv  22020  mdegle0  23074  isppw2  24090  cusgrauvtxb  25272  eleclclwwlkn  25609  eupath2lem1  25753  hvaddcan  26771  eigre  27536  xrge0iifcnv  28787  sgn0bi  29466  signswch  29498  bnj1468  29705  br1steqg  30464  br2ndeqg  30465  subtr2  31019  nn0prpwlem  31026  nn0prpw  31027  bj-axext3  31428  ftc1anclem6  32066  zindbi  35838  expdioph  35922  islssfg2  35973  eliunov2  36315  pm14.122b  36817