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  2288  axext3  2423  axext3OLD  2424  bm1.1  2426  bm1.1OLD  2427  eqeq1dALT  2446  eqeq1OLD  2448  pm13.183  3226  elabgt  3229  elrab3t  3242  mob  3267  sbctt  3384  sbcabel  3402  isoeq2  6201  caovcang  6461  domunfican  7795  axacndlem4  8991  axacnd  8993  expeq0  12178  prmdvdsexp  14237  isacs  15030  acsfn  15038  tsrlemax  15829  odeq  16553  isslw  16607  isabv  17447  t0sep  19803  xkopt  20134  kqt0lem  20215  r0sep  20227  nrmr0reg  20228  ismet  20804  isxmet  20805  stdbdxmet  20996  xrsxmet  21292  iccpnfcnv  21422  mdegle0  22455  isppw2  23367  cusgrauvtxb  24474  eleclclwwlkn  24811  eupath2lem1  24955  hvaddcan  25965  eigre  26732  xrge0iifcnv  27893  sgn0bi  28464  signswch  28496  relexpind  29041  dfrtrclrec2  29044  ftc1anclem6  30071  subtr2  30109  nn0prpwlem  30116  nn0prpw  30117  zindbi  30858  expdioph  30941  islssfg2  30993  pm14.122b  31284  bnj1468  33772  bj-axext3  34237