Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  imbi1d Unicode version

Theorem imbi1d 230
 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 157 . . 3
32imim1d 75 . 2
41biimpd 143 . . 3
54imim1d 75 . 2
63, 5impbid 128 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 104 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  imbi12d  233  imbi1  235  imim21b  251  pm5.33  599  imordc  883  drsb1  1772  ax11v2  1793  ax11v  1800  ax11ev  1801  equs5or  1803  raleqf  2626  rspceaimv  2802  alexeq  2816  mo2icl  2868  sbc19.21g  2982  csbiebg  3048  ralss  3169  ifmdc  3515  ssuni  3767  intmin4  3808  ssexg  4076  pocl  4234  frforeq1  4274  frforeq2  4276  frind  4283  ontr2exmid  4449  elirr  4465  en2lp  4478  tfisi  4510  vtoclr  4596  sosng  4621  fun11  5199  funimass4  5481  dff13  5678  f1mpt  5681  isopolem  5732  oprabid  5812  caovcan  5944  caoftrn  6016  dfsmo2  6193  tfr1onlemsucfn  6246  tfr1onlemsucaccv  6247  tfr1onlembxssdm  6249  tfr1onlembfn  6250  tfr1onlemres  6255  tfrcllemsucfn  6259  tfrcllemsucaccv  6260  tfrcllembxssdm  6262  tfrcllembfn  6263  tfrcllemres  6268  tfrcl  6270  qliftfun  6520  ecoptocl  6525  ecopovtrn  6535  ecopovtrng  6538  dom2lem  6675  ssfiexmid  6779  domfiexmid  6781  findcard  6791  findcard2  6792  findcard2s  6793  fiintim  6827  supmoti  6890  eqsupti  6893  suplubti  6897  supisoex  6906  isomnimap  7019  ismkvmap  7038  iswomnimap  7050  ltsonq  7250  prarloclem3  7349  suplocexpr  7577  lttrsr  7614  mulextsr1  7633  suplocsrlem  7660  axpre-lttrn  7736  axpre-mulext  7740  axcaucvglemres  7751  axpre-suploclemres  7753  axpre-suploc  7754  prime  9194  raluz  9420  indstr  9435  supinfneg  9437  infsupneg  9438  fz1sbc  9927  exbtwnzlemshrink  10077  rebtwn2zlemshrink  10082  apexp1  10516  zfz1iso  10636  caucvgre  10805  maxleast  11037  rexanre  11044  rexico  11045  minmax  11053  xrminmax  11086  addcn2  11131  mulcn2  11133  cn1lem  11135  zsupcllemstep  11694  zsupcllemex  11695  bezoutlemmain  11742  dfgcd2  11758  exprmfct  11874  prmdvdsexpr  11884  sqrt2irr  11896  pw2dvdslemn  11899  istopg  12225  lmbr  12441  metcnp  12740  addcncntoplem  12779  bj-rspgt  13184  bdssexg  13293  strcollnft  13373  sscoll2  13377
 Copyright terms: Public domain W3C validator