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

Theorem biimpi 117
Description: Infer an implication from a logical equivalence. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
biimpi.1  |-  ( ph  <->  ps )
Assertion
Ref Expression
biimpi  |-  ( ph  ->  ps )

Proof of Theorem biimpi
StepHypRef Expression
1 biimpi.1 . 2  |-  ( ph  <->  ps )
2 bi1 115 . 2  |-  ( (
ph 
<->  ps )  ->  ( ph  ->  ps ) )
31, 2ax-mp 7 1  |-  ( ph  ->  ps )
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  2739  euind  2751  reuind  2767  ssel  2967  unssd  3147  ssind  3189  unssdif  3200  ss0  3285  prprc  3508  trint  3897  snexprc  3966  pocl  4068  sotritrieq  4090  frirrg  4115  unexg  4206  reusv3i  4219  ordtriexmid  4275  ordtri2orexmid  4276  preleq  4307  0elsucexmid  4317  ordpwsucexmid  4322  ordtri2or2exmid  4324  elnn  4356  brrelex12  4409  elrel  4470  xpssres  4673  elres  4674  coi2  4865  iotabi  4904  uniabio  4905  nfunv  4961  funun  4972  funcnv3  4989  funimass1  5004  imain  5009  funssxp  5088  f1o00  5189  fsn2  5365  isoselem  5487  oprabid  5565  brabvv  5579  1stdm  5836  f1o2ndf1  5877  poxp  5881  nntri3or  6103  nntri1  6105  ensym  6292  snnen2oprc  6354  phplem4on  6360  fidceq  6361  php5fin  6370  fisbth  6371  fin0  6373  fin0or  6374  diffisn  6381  fientri3  6384  enq0sym  6588  enq0tr  6590  prarloclem3  6653  nqprl  6707  nqpru  6708  addnqprlemrl  6713  addnqprlemru  6714  addnqprlemfl  6715  addnqprlemfu  6716  mulnqprlemrl  6729  mulnqprlemru  6730  mulnqprlemfl  6731  mulnqprlemfu  6732  ltexprlemfl  6765  ltexprlemfu  6767  recexprlemopl  6781  recexprlemopu  6783  aptipr  6797  cauappcvgprlemladdfu  6810  cauappcvgprlemladdfl  6811  caucvgprlemladdfu  6833  caucvgprprlemexbt  6862  srpospr  6925  elrealeu  6964  axarch  7023  axcaucvglemres  7031  nn0ge2m1nn  8299  elnn0z  8315  peano2z  8338  uzm1  8599  qapne  8671  rpregt0  8694  rpnegap  8713  elfz1end  9021  1fv  9098  elfzonlteqm1  9168  qtri3or  9200  qbtwnzlemshrink  9206  rebtwn2zlemshrink  9210  ioom  9217  modfzo0difsn  9345  modsumfzodifsn  9346  addmodlteq  9348  frecfzennn  9367  iser0  9415  expival  9422  facp1  9598  faclbnd  9609  bcn1  9626  sqrt0  9831  resqrexlemfp1  9836  cau3lem  9941  climcaucn  10101  ex-ceil  10280  bj-sucexg  10429  bj-om  10448  bj-inf2vnlem1  10482
  Copyright terms: Public domain W3C validator