Theorem bibi1d 320

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 319	. 2 |- ( ph -> ( ( th <-> ps ) <-> ( th <-> ch ) ) )
3		bicom 203	. 2 |- ( ( ps <-> th ) <-> ( th <-> ps ) )
4		bicom 203	. 2 |- ( ( ch <-> th ) <-> ( th <-> ch ) )
5	2, 3, 4	3bitr4g 291	1 |- ( ph -> ( ( ps <-> th ) <-> ( ch <-> th ) ) )

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

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 188

This theorem is referenced by:  bibi12d  322  bibi1  328  biass  360  eubid  2284  axext3  2402  axext3OLD  2403  bm1.1  2405  bm1.1OLD  2406  eqeq1dALT  2425  eqeq1OLD  2427  pm13.183  3212  elabgt  3215  elrab3t  3228  mob  3253  sbctt  3362  sbcabel  3377  isoeq2  6223  caovcang  6481  domunfican  7847  axacndlem4  9036  axacnd  9038  expeq0  12302  dfrtrclrec2  13109  relexpind  13116  prmdvdsexp  14655  isacs  15545  acsfn  15553  tsrlemax  16454  odeq  17187  isslw  17248  isabv  18035  t0sep  20327  xkopt  20657  kqt0lem  20738  r0sep  20750  nrmr0reg  20751  ismet  21325  isxmet  21326  stdbdxmet  21517  xrsxmet  21814  iccpnfcnv  21959  mdegle0  23013  isppw2  24029  cusgrauvtxb  25210  eleclclwwlkn  25547  eupath2lem1  25691  hvaddcan  26709  eigre  27474  xrge0iifcnv  28735  sgn0bi  29414  signswch  29446  bnj1468  29653  br1steqg  30411  br2ndeqg  30412  subtr2  30964  nn0prpwlem  30971  nn0prpw  30972  bj-axext3  31341  ftc1anclem6  31936  zindbi  35714  expdioph  35798  islssfg2  35849  eliunov2  36131  pm14.122b  36632