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  6414  enq0tr  6416  prarloclem3  6479  addnqpr1lemrl  6537  addnqpr1lemru  6538  addnqpr1lemil  6539  addnqpr1lemiu  6540  ltexprlemfl  6581  ltexprlemfu  6583  recexprlemopl  6595  recexprlemopu  6597  aptipr  6611  axarch  6733  nn0ge2m1nn  7978  elnn0z  7994  peano2z  8017  uzm1  8239  qapne  8310  rpregt0  8331  rpnegap  8350  elfz1end  8649  1fv  8726  elfzonlteqm1  8796  frecfzennn  8844  expival  8871  bj-sucexg  9307  bj-om  9325  bj-inf2vnlem1  9354
  Copyright terms: Public domain W3C validator