Theorem bibi1d 319

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 318	. 2 |- ( ph -> ( ( th <-> ps ) <-> ( th <-> ch ) ) )
3		bicom 200	. 2 |- ( ( ps <-> th ) <-> ( th <-> ps ) )
4		bicom 200	. 2 |- ( ( ch <-> th ) <-> ( th <-> ch ) )
5	2, 3, 4	3bitr4g 288	1 |- ( ph -> ( ( ps <-> th ) <-> ( ch <-> th ) ) )

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

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 185

This theorem is referenced by:  bibi12d  321  bibi1  327  biass  359  eubid  2296  axext3  2447  axext3OLD  2448  bm1.1  2450  bm1.1OLD  2451  eqeq1dALT  2470  eqeq1OLD  2472  pm13.183  3244  elabgt  3247  elrab3t  3260  mob  3285  sbctt  3402  sbcabel  3420  isoeq2  6204  caovcang  6460  domunfican  7793  axacndlem4  8988  axacnd  8990  expeq0  12164  prmdvdsexp  14114  isacs  14906  acsfn  14914  tsrlemax  15707  odeq  16380  isslw  16434  isabv  17268  t0sep  19619  xkopt  19919  kqt0lem  20000  r0sep  20012  nrmr0reg  20013  ismet  20589  isxmet  20590  stdbdxmet  20781  xrsxmet  21077  iccpnfcnv  21207  mdegle0  22240  isppw2  23145  cusgrauvtxb  24200  eleclclwwlkn  24537  eupath2lem1  24681  hvaddcan  25691  eigre  26458  xrge0iifcnv  27579  sgn0bi  28154  signswch  28186  relexpind  28566  dfrtrclrec2  28569  ftc1anclem6  29700  subtr2  29738  nn0prpwlem  29745  nn0prpw  29746  zindbi  30514  expdioph  30597  islssfg2  30649  pm14.122b  30936  bnj1468  33001  bj-axext3  33453