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

Theorem impbid1 130
 Description: Infer an equivalence from two implications. (Contributed by NM, 6-Mar-2007.)
Hypotheses
Ref Expression
impbid1.1
impbid1.2
Assertion
Ref Expression
impbid1

Proof of Theorem impbid1
StepHypRef Expression
1 impbid1.1 . 2
2 impbid1.2 . . 3
32a1i 9 . 2
41, 3impbid 120 1
 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-ia2 100  ax-ia3 101 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  impbid2  131  iba  284  ibar  285  pm4.81dc  814  pm5.63dc  853  pm4.83dc  858  pm5.71dc  868  19.33b2  1520  19.9t  1533  sb4b  1715  a16gb  1745  euor2  1958  eupickbi  1982  ceqsalg  2582  eqvincg  2668  csbprc  3262  undif4  3284  sssnm  3525  sneqbg  3534  opthpr  3543  elpwuni  3741  eusv2i  4187  reusv3  4192  iunpw  4211  suc11g  4281  xpid11m  4557  ssxpbm  4756  ssxp1  4757  ssxp2  4758  xp11m  4759  2elresin  5010  mpteqb  5261  f1fveq  5411  f1elima  5412  f1imass  5413  fliftf  5439  iserd  6132  ecopovtrn  6203  ecopover  6204  ecopovtrng  6206  ecopoverg  6207  fopwdom  6310  addcanpig  6432  mulcanpig  6433  srpospr  6867  readdcan  7153  cnegexlem1  7186  addcan  7191  addcan2  7192  neg11  7262  negreb  7276  add20  7469  cru  7593  mulcanapd  7642  uz11  8495  eqreznegel  8549  lbzbi  8551  xneg11  8747  elioc2  8805  elico2  8806  elicc2  8807  fzopth  8924  2ffzeq  8998  flqidz  9128  frec2uzrand  9191  cj11  9505  sqrt0  9602  recan  9705  algcvgblem  9888  bj-peano4  10080  bj-nn0sucALT  10103
 Copyright terms: Public domain W3C validator