NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  imbi1d Unicode version

Theorem imbi1d 308
Description: Deduction adding a consequent to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 17-Sep-2013.)
Hypothesis
Ref Expression
imbid.1
Assertion
Ref Expression
imbi1d

Proof of Theorem imbi1d
StepHypRef Expression
1 imbid.1 . . . 4
21biimprd 214 . . 3
32imim1d 69 . 2
41biimpd 198 . . 3
54imim1d 69 . 2
63, 5impbid 183 1
Colors of variables: wff setvar class
Syntax hints:   wi 4   wb 176
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
This theorem is referenced by:  imbi12d  311  imbi1  313  imim21b  356  pm5.33  848  con3th  924  ax12bOLD  1690  19.21t  1795  ax11v2  1992  drsb1  2022  ax11vALT  2097  ax11inda  2200  ax11v2-o  2201  ralcom2  2775  raleqf  2803  alexeq  2968  mo2icl  3015  sbc19.21g  3110  csbiebg  3175  ralss  3332  r19.37zv  3646  ssuni  3913  intmin4  3955  eqpw1uni  4330  nnsucelr  4428  nndisjeq  4429  preaddccan2lem1  4454  preaddccan2  4455  leltfintr  4458  ssfin  4470  ncfinlower  4483  sfinltfin  4535  spfinsfincl  4539  vfinspss  4551  vtoclr  4816  fun11  5159  funimass4  5368  dff13  5471  oprabid  5550  caovcan  5628  clos1conn  5879  trd  5921  frd  5922  extd  5923  antird  5928  antid  5929  ecoptocl  5996  enprmapc  6083  nclenn  6249  addccan2nc  6265  nchoicelem12  6300  nchoicelem16  6304  nchoicelem17  6305  fnfrec  6320
  Copyright terms: Public domain W3C validator