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

Theorem biimpi 113
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 111 . 2  |-  ( (
ph 
<->  ps )  ->  ( ph  ->  ps ) )
31, 2ax-mp 7 1  |-  ( ph  ->  ps )
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  679  pm2.32  686  stabnot  741  exmiddc  744  pm2.1dc  745  oranim  807  stabtestimpdc  824  pm5.75  869  rnlem  883  simp1bi  919  simp2bi  920  simp3bi  921  syl3an1b  1171  syl3an2b  1172  syl3an3b  1173  exalim  1391  nford  1459  stdpc5  1476  sbbii  1648  sb9i  1856  eu5  1947  exmoeudc  1963  eqeq1  2046  eleq2  2101  nner  2210  rexalim  2319  gencbvex  2600  gencbval  2602  moeq  2716  euind  2728  reuind  2744  eqsbc3r  2819  ssel  2939  unssd  3119  ssind  3161  unssdif  3172  ss0  3257  prprc  3480  trint  3869  snexprc  3938  pocl  4040  sotritrieq  4062  frirrg  4087  unexg  4178  reusv3i  4191  ordtriexmid  4247  ordtri2orexmid  4248  preleq  4279  0elsucexmid  4289  ordpwsucexmid  4294  ordtri2or2exmid  4296  elnn  4328  brrelex12  4381  elrel  4442  xpssres  4645  elres  4646  coi2  4837  iotabi  4876  uniabio  4877  nfunv  4933  funun  4944  funcnv3  4961  funimass1  4976  imain  4981  funssxp  5060  f1o00  5161  fsn2  5337  isoselem  5459  oprabid  5537  brabvv  5551  1stdm  5808  f1o2ndf1  5849  poxp  5853  nntri3or  6072  nntri1  6074  ensym  6261  snnen2oprc  6323  phplem4on  6329  fidceq  6330  php5fin  6339  fisbth  6340  fin0  6342  fin0or  6343  diffisn  6350  fientri3  6353  enq0sym  6530  enq0tr  6532  prarloclem3  6595  nqprl  6649  nqpru  6650  addnqprlemrl  6655  addnqprlemru  6656  addnqprlemfl  6657  addnqprlemfu  6658  mulnqprlemrl  6671  mulnqprlemru  6672  mulnqprlemfl  6673  mulnqprlemfu  6674  ltexprlemfl  6707  ltexprlemfu  6709  recexprlemopl  6723  recexprlemopu  6725  aptipr  6739  cauappcvgprlemladdfu  6752  cauappcvgprlemladdfl  6753  caucvgprlemladdfu  6775  caucvgprprlemexbt  6804  srpospr  6867  elrealeu  6906  axarch  6965  axcaucvglemres  6973  nn0ge2m1nn  8242  elnn0z  8258  peano2z  8281  uzm1  8503  qapne  8574  rpregt0  8596  rpnegap  8615  elfz1end  8919  1fv  8996  elfzonlteqm1  9066  qtri3or  9098  qbtwnzlemshrink  9104  rebtwn2zlemshrink  9108  frecfzennn  9203  iser0  9250  expival  9257  sqrt0  9602  resqrexlemfp1  9607  cau3lem  9710  climcaucn  9870  ex-ceil  9896  bj-sucexg  10042  bj-om  10061  bj-inf2vnlem1  10095
  Copyright terms: Public domain W3C validator