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  775  exmiddc  778  pm2.1dc  779  oranim  841  stabtestimpdc  858  pm5.75  904  rnlem  918  simp1bi  954  simp2bi  955  simp3bi  956  syl3an1b  1206  syl3an2b  1207  syl3an3b  1208  exalim  1432  nford  1500  stdpc5  1517  sbbii  1690  sb9i  1899  eu5  1990  exmoeudc  2006  eqeq1  2089  eleq2  2146  nner  2253  rexalim  2367  gencbvex  2656  gencbval  2658  moeq  2778  euind  2790  reuind  2806  ssel  3004  unssd  3160  ssind  3208  unssdif  3217  ss0  3305  prprc  3526  trint  3916  snexprc  3984  undifexmid  3991  exmidundif  3998  pocl  4093  sotritrieq  4115  frirrg  4140  unexg  4231  reusv3i  4244  ordtriexmid  4300  ordtri2orexmid  4301  preleq  4333  0elsucexmid  4343  ordpwsucexmid  4348  ordtri2or2exmid  4349  elnn  4382  brrelex12  4436  elrel  4497  xpssres  4703  elres  4704  coi2  4900  iotabi  4942  uniabio  4943  nfunv  4999  funun  5010  funcnv3  5028  funimass1  5043  imain  5048  funssxp  5128  f0dom0  5151  f1o00  5235  fsn2  5412  isoselem  5537  oprabid  5615  brabvv  5629  1stdm  5886  f1o2ndf1  5927  poxp  5931  rdgon  6082  frecfcllem  6100  nntri3or  6185  nntri1  6188  ensym  6427  xpen  6490  snnen2oprc  6505  phplem4on  6512  fict  6513  fidceq  6514  infiexmid  6522  php5fin  6527  fisbth  6528  fin0  6530  fin0or  6531  diffisn  6538  infnfi  6540  en2eqpr  6549  exmidpw  6550  fientri3  6551  unsnfi  6555  unsnfidcex  6556  unsnfidcel  6557  undifdcss  6559  ssfidc  6568  relcnvfi  6574  eqinfti  6621  djulclb  6653  enomnilem  6698  finomni  6700  exmidomni  6702  enq0sym  6893  enq0tr  6895  prarloclem3  6958  nqprl  7012  nqpru  7013  addnqprlemrl  7018  addnqprlemru  7019  addnqprlemfl  7020  addnqprlemfu  7021  mulnqprlemrl  7034  mulnqprlemru  7035  mulnqprlemfl  7036  mulnqprlemfu  7037  ltexprlemfl  7070  ltexprlemfu  7072  recexprlemopl  7086  recexprlemopu  7088  aptipr  7102  cauappcvgprlemladdfu  7115  cauappcvgprlemladdfl  7116  caucvgprlemladdfu  7138  caucvgprprlemexbt  7167  srpospr  7230  elrealeu  7269  axarch  7328  axcaucvglemres  7336  nn0ge2m1nn  8624  elnn0z  8658  peano2z  8681  uzm1  8943  qapne  9018  rpregt0  9041  rpnegap  9060  elfz1end  9363  1fv  9439  elfzonlteqm1  9509  qtri3or  9542  exbtwnzlemshrink  9548  rebtwn2zlemshrink  9553  ioom  9560  modfzo0difsn  9690  modsumfzodifsn  9691  addmodlteq  9693  frecfzennn  9721  iser0  9786  facp1  9972  faclbnd  9983  bcn1  10000  hashennnuni  10021  hashcl  10023  hashfz1  10025  hashen  10026  fihashdom  10045  hashun  10047  sqrt0  10263  resqrexlemfp1  10268  cau3lem  10373  climcaucn  10561  bezoutlemzz  10770  dfgcd3  10778  lcmcllem  10828  prmind2  10881  prm2orodd  10887  sqrt2irrap  10937  ex-ceil  10996  bj-sucexg  11155  bj-om  11174  bj-inf2vnlem1  11207
  Copyright terms: Public domain W3C validator