ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  biimpi Structured version   GIF 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  6415  enq0tr  6417  prarloclem3  6480  nqprl  6533  addnqprlemrl  6538  addnqprlemru  6539  addnqprlemfl  6540  addnqprlemfu  6541  ltexprlemfl  6583  ltexprlemfu  6585  recexprlemopl  6597  recexprlemopu  6599  aptipr  6613  cauappcvgprlemladdfu  6626  cauappcvgprlemladdfl  6627  caucvgprlemladdfu  6648  axarch  6773  nn0ge2m1nn  8018  elnn0z  8034  peano2z  8057  uzm1  8279  qapne  8350  rpregt0  8371  rpnegap  8390  elfz1end  8689  1fv  8766  elfzonlteqm1  8836  frecfzennn  8884  expival  8911  sqrt0  9213  bj-sucexg  9377  bj-om  9396  bj-inf2vnlem1  9430
  Copyright terms: Public domain W3C validator