Theorem bibi2d 318

Description: Deduction adding a biconditional to the left in an equivalence. (Contributed by NM, 11-May-1993.) (Proof shortened by Wolf Lammen, 19-May-2013.)

Hypothesis

Ref	Expression
imbid.1

Assertion

Ref	Expression
bibi2d

Proof of Theorem bibi2d

Step	Hyp	Ref	Expression
1		imbid.1	. . . . 5
2	1	pm5.74i 245	. . . 4
3	2	bibi2i 313	. . 3
4		pm5.74 244	. . 3
5		pm5.74 244	. . 3
6	3, 4, 5	3bitr4i 277	. 2
7	6	pm5.74ri 246	1

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

This theorem is referenced by:  bibi1d  319  bibi12d  321  biantr  931  bimsc1  938  eujust  2284  eujustALT  2285  euf  2292  reu6i  3290  sbc2or  3336  axrep1  4564  axrep2  4565  axrep3  4566  zfrepclf  4569  axsep2  4574  zfauscl  4575  copsexg  4737  copsexgOLD  4738  euotd  4753  cnveq0  5468  iotaval  5567  iota5  5576  eufnfv  6146  isoeq1  6215  isoeq3  6217  isores2  6229  isores3  6231  isotr  6232  isoini2  6235  riota5f  6282  caovordg  6482  caovord  6486  dfoprab4f  6858  seqomlem2  7135  xpf1o  7699  aceq0  8520  dfac5  8530  zfac  8861  zfcndrep  9013  zfcndac  9018  ltasr  9498  axpre-ltadd  9565  absmod0  13136  absz  13144  smuval2  14132  prmdvdsexp  14255  isacs2  15050  isacs1i  15054  mreacs  15055  abvfval  17467  abvpropd  17491  isclo2  19589  t0sep  19825  kqt0lem  20237  r0sep  20249  iccpnfcnv  21444  rolle  22391  fargshiftfo  24638  2wlkeq  24707  ismndo2  25347  eigre  26754  fgreu  27513  fcnvgreu  27514  xrge0iifcnv  27915  cvmlift2lem13  28760  iota5f  29102  nn0prpwlem  30140  nn0prpw  30141  mrefg2  30639  zindbi  30882  jm2.19lem3  30933  iotavalb  31337  bj-axrep1  34374  bj-axrep2  34375  bj-axrep3  34376  bj-axsep2  34493  islaut  35807  ispautN  35823

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