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

Assertion

Ref	Expression
bibi1d

Proof of Theorem bibi1d

Step	Hyp	Ref	Expression
1		imbid.1	. . 3
2	1	bibi2d 318	. 2
3		bicom 200	. 2
4		bicom 200	. 2
5	2, 3, 4	3bitr4g 288	1

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

This theorem is referenced by:  bibi12d  321  bibi1  327  biass  359  eubid  2302  axext3  2437  axext3OLD  2438  bm1.1  2440  bm1.1OLD  2441  eqeq1dALT  2460  eqeq1OLD  2462  pm13.183  3240  elabgt  3243  elrab3t  3256  mob  3281  sbctt  3398  sbcabel  3416  isoeq2  6216  caovcang  6476  domunfican  7813  axacndlem4  9009  axacnd  9011  expeq0  12196  prmdvdsexp  14255  isacs  15048  acsfn  15056  tsrlemax  15850  odeq  16574  isslw  16628  isabv  17468  t0sep  19825  xkopt  20156  kqt0lem  20237  r0sep  20249  nrmr0reg  20250  ismet  20826  isxmet  20827  stdbdxmet  21018  xrsxmet  21314  iccpnfcnv  21444  mdegle0  22477  isppw2  23389  cusgrauvtxb  24496  eleclclwwlkn  24833  eupath2lem1  24977  hvaddcan  25987  eigre  26754  xrge0iifcnv  27915  sgn0bi  28486  signswch  28518  relexpind  29063  dfrtrclrec2  29066  ftc1anclem6  30095  subtr2  30133  nn0prpwlem  30140  nn0prpw  30141  zindbi  30882  expdioph  30965  islssfg2  31017  pm14.122b  31330  bnj1468  33904  bj-axext3  34354

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