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

Theorem biimpi 117
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 115 . 2 ((𝜑𝜓) → (𝜑𝜓))
31, 2ax-mp 7 1 (𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  sylbi  118  biimpri  128  sylib  131  mpbi  137  syl5bi  145  syl6ib  154  syl7bi  158  syl8ib  159  bitri  177  simplbi  263  simprbi  264  sylanb  272  sylan2b  275  anc2l  314  sylanblc  400  orbi2i  689  pm2.32  696  stabnot  752  exmiddc  755  pm2.1dc  756  oranim  818  stabtestimpdc  835  pm5.75  880  rnlem  894  simp1bi  930  simp2bi  931  simp3bi  932  syl3an1b  1182  syl3an2b  1183  syl3an3b  1184  exalim  1407  nford  1475  stdpc5  1492  sbbii  1664  sb9i  1872  eu5  1963  exmoeudc  1979  eqeq1  2062  eleq2  2117  nner  2224  rexalim  2336  gencbvex  2617  gencbval  2619  moeq  2738  euind  2750  reuind  2766  ssel  2966  unssd  3146  ssind  3188  unssdif  3199  ss0  3284  prprc  3507  trint  3896  snexprc  3965  pocl  4067  sotritrieq  4089  frirrg  4114  unexg  4205  reusv3i  4218  ordtriexmid  4274  ordtri2orexmid  4275  preleq  4306  0elsucexmid  4316  ordpwsucexmid  4321  ordtri2or2exmid  4323  elnn  4355  brrelex12  4408  elrel  4469  xpssres  4672  elres  4673  coi2  4864  iotabi  4903  uniabio  4904  nfunv  4960  funun  4971  funcnv3  4988  funimass1  5003  imain  5008  funssxp  5087  f1o00  5188  fsn2  5364  isoselem  5486  oprabid  5564  brabvv  5578  1stdm  5835  f1o2ndf1  5876  poxp  5880  nntri3or  6102  nntri1  6104  ensym  6291  snnen2oprc  6353  phplem4on  6359  fidceq  6360  php5fin  6369  fisbth  6370  fin0  6372  fin0or  6373  diffisn  6380  fientri3  6383  enq0sym  6587  enq0tr  6589  prarloclem3  6652  nqprl  6706  nqpru  6707  addnqprlemrl  6712  addnqprlemru  6713  addnqprlemfl  6714  addnqprlemfu  6715  mulnqprlemrl  6728  mulnqprlemru  6729  mulnqprlemfl  6730  mulnqprlemfu  6731  ltexprlemfl  6764  ltexprlemfu  6766  recexprlemopl  6780  recexprlemopu  6782  aptipr  6796  cauappcvgprlemladdfu  6809  cauappcvgprlemladdfl  6810  caucvgprlemladdfu  6832  caucvgprprlemexbt  6861  srpospr  6924  elrealeu  6963  axarch  7022  axcaucvglemres  7030  nn0ge2m1nn  8298  elnn0z  8314  peano2z  8337  uzm1  8598  qapne  8670  rpregt0  8693  rpnegap  8712  elfz1end  9020  1fv  9097  elfzonlteqm1  9167  qtri3or  9199  qbtwnzlemshrink  9205  rebtwn2zlemshrink  9209  ioom  9216  modfzo0difsn  9344  modsumfzodifsn  9345  addmodlteq  9347  frecfzennn  9366  iser0  9414  expival  9421  facp1  9597  faclbnd  9608  bcn1  9625  sqrt0  9830  resqrexlemfp1  9835  cau3lem  9940  climcaucn  10100  ex-ceil  10259  bj-sucexg  10408  bj-om  10427  bj-inf2vnlem1  10461
  Copyright terms: Public domain W3C validator