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

Theorem biimpi 113
Description: Infer an implication from a logical equivalence. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
biimpi.1
Assertion
Ref Expression
biimpi

Proof of Theorem biimpi
StepHypRef Expression
1 biimpi.1 . 2
2 bi1 111 . 2
31, 2ax-mp 7 1
Colors of variables: wff set class
Syntax hints:   wi 4   wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  sylbi  114  biimpri  124  sylib  127  mpbi  133  syl5bi  141  syl6ib  150  syl7bi  154  syl8ib  155  bitri  173  simplbi  259  simprbi  260  sylanb  268  sylan2b  271  anc2l  310  orbi2i  678  pm2.32  685  stabnot  740  exmiddc  743  pm2.1dc  744  oranim  806  stabtestimpdc  823  pm5.75  868  rnlem  882  simp1bi  918  simp2bi  919  simp3bi  920  syl3an1b  1170  syl3an2b  1171  syl3an3b  1172  exalim  1388  nford  1456  stdpc5  1473  sbbii  1645  sb9i  1853  eu5  1944  exmoeudc  1960  eqeq1  2043  eleq2  2098  nner  2207  rexalim  2313  gencbvex  2594  gencbval  2596  moeq  2710  euind  2722  reuind  2738  eqsbc3r  2813  ssel  2933  unssd  3113  ssind  3155  unssdif  3166  ss0  3251  prprc  3471  trint  3860  snexprc  3929  pocl  4031  sotritrieq  4053  unexg  4144  reusv3i  4157  ordtriexmid  4210  ordtri2orexmid  4211  preleq  4233  ordpwsucexmid  4246  elnn  4271  brrelex12  4324  elrel  4385  xpssres  4588  elres  4589  coi2  4780  iotabi  4819  uniabio  4820  nfunv  4876  funun  4887  funcnv3  4904  funimass1  4919  imain  4924  funssxp  5003  f1o00  5104  fsn2  5280  isoselem  5402  oprabid  5480  brabvv  5493  1stdm  5750  f1o2ndf1  5791  poxp  5794  nntri3or  6011  nntri1  6013  ensym  6197  enq0sym  6414  enq0tr  6416  prarloclem3  6479  nqprl  6532  addnqprlemrl  6537  addnqprlemru  6538  addnqprlemfl  6539  addnqprlemfu  6540  ltexprlemfl  6582  ltexprlemfu  6584  recexprlemopl  6596  recexprlemopu  6598  aptipr  6612  cauappcvgprlemladdfu  6625  cauappcvgprlemladdfl  6626  axarch  6753  nn0ge2m1nn  7998  elnn0z  8014  peano2z  8037  uzm1  8259  qapne  8330  rpregt0  8351  rpnegap  8370  elfz1end  8669  1fv  8746  elfzonlteqm1  8816  frecfzennn  8864  expival  8891  sqrt0  9193  bj-sucexg  9353  bj-om  9371  bj-inf2vnlem1  9400
  Copyright terms: Public domain W3C validator