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

Theorem biimpi 118
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 116 . 2 ((𝜑𝜓) → (𝜑𝜓))
31, 2ax-mp 7 1 (𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  sylbi  119  sylib  120  sylbb  121  biimpri  131  mpbi  143  syl5bi  150  syl6ib  159  syl7bi  163  syl8ib  164  bitri  182  simplbi  268  simprbi  269  sylanb  278  sylan2b  281  anc2l  320  sylanblc  406  orbi2i  712  pm2.32  719  stabnot  776  imanst  777  exmiddc  780  pm2.1dc  781  oranim  843  stabtestimpdc  860  pm5.75  906  rnlem  920  simp1bi  956  simp2bi  957  simp3bi  958  syl3an1b  1208  syl3an2b  1209  syl3an3b  1210  exalim  1434  nford  1502  stdpc5  1519  sbbii  1692  sb9i  1901  eu5  1992  exmoeudc  2008  eqeq1  2091  eleq2  2148  nner  2255  rexalim  2369  gencbvex  2659  gencbval  2661  moeq  2781  euind  2793  reuind  2809  ssel  3008  unssd  3165  ssind  3213  unssdif  3223  ss0  3311  prprc  3535  trint  3926  snexprc  3995  undifexmid  4002  exmidundif  4009  pocl  4104  sotritrieq  4126  frirrg  4151  unexg  4242  reusv3i  4255  ordtriexmid  4311  ordtri2orexmid  4312  preleq  4344  0elsucexmid  4354  ordpwsucexmid  4359  ordtri2or2exmid  4360  elnn  4393  brrelex12  4447  elrel  4508  xpssres  4714  elres  4715  coi2  4913  iotabi  4955  uniabio  4956  nfunv  5012  funun  5023  funcnv3  5041  funimass1  5056  imain  5061  funssxp  5144  f0dom0  5167  f1o00  5251  fsn2  5434  isoselem  5560  oprabid  5638  brabvv  5652  1stdm  5909  f1o2ndf1  5950  poxp  5954  rdgon  6105  frecfcllem  6123  nntri3or  6208  nntri1  6211  ensym  6450  xpen  6513  snnen2oprc  6528  phplem4on  6535  fict  6536  fidceq  6537  infiexmid  6545  php5fin  6550  fisbth  6551  fin0  6553  fin0or  6554  diffisn  6561  infnfi  6563  en2eqpr  6575  exmidpw  6576  fientri3  6577  unsnfi  6581  unsnfidcex  6582  unsnfidcel  6583  undifdcss  6585  ssfidc  6594  relcnvfi  6600  eqinfti  6659  djulclb  6691  enomnilem  6738  finomni  6740  exmidomni  6742  enq0sym  6935  enq0tr  6937  prarloclem3  7000  nqprl  7054  nqpru  7055  addnqprlemrl  7060  addnqprlemru  7061  addnqprlemfl  7062  addnqprlemfu  7063  mulnqprlemrl  7076  mulnqprlemru  7077  mulnqprlemfl  7078  mulnqprlemfu  7079  ltexprlemfl  7112  ltexprlemfu  7114  recexprlemopl  7128  recexprlemopu  7130  aptipr  7144  cauappcvgprlemladdfu  7157  cauappcvgprlemladdfl  7158  caucvgprlemladdfu  7180  caucvgprprlemexbt  7209  srpospr  7272  elrealeu  7311  axarch  7370  axcaucvglemres  7378  nn0ge2m1nn  8666  elnn0z  8696  peano2z  8719  uzm1  8981  qapne  9056  rpregt0  9079  rpnegap  9098  elfz1end  9401  1fv  9478  elfzonlteqm1  9549  qtri3or  9582  exbtwnzlemshrink  9588  rebtwn2zlemshrink  9593  ioom  9600  modfzo0difsn  9730  modsumfzodifsn  9731  addmodlteq  9733  frecfzennn  9761  iseqf1olemstep  9834  iser0  9847  facp1  10034  faclbnd  10045  bcn1  10062  hashennnuni  10083  hashcl  10085  hashfz1  10087  hashen  10088  fihashdom  10107  hashun  10109  zfz1isolem1  10141  zfz1iso  10142  sqrt0  10332  resqrexlemfp1  10337  cau3lem  10442  climcaucn  10630  bezoutlemzz  10866  dfgcd3  10874  lcmcllem  10924  prmind2  10977  prm2orodd  10983  sqrt2irrap  11033  ex-ceil  11092  bj-sucexg  11251  bj-om  11270  bj-inf2vnlem1  11303
  Copyright terms: Public domain W3C validator