ILE Home 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  813  pm5.63dc  852  pm4.83dc  857  pm5.71dc  867  19.33b2  1517  19.9t  1530  sb4b  1712  a16gb  1742  euor2  1955  eupickbi  1979  ceqsalg  2576  eqvincg  2662  csbprc  3256  undif4  3278  sssnm  3516  sneqbg  3525  opthpr  3534  elpwuni  3732  eusv2i  4153  reusv3  4158  iunpw  4177  suc11g  4235  xpid11m  4500  ssxpbm  4699  ssxp1  4700  ssxp2  4701  xp11m  4702  2elresin  4953  mpteqb  5204  f1fveq  5354  f1elima  5355  f1imass  5356  fliftf  5382  iserd  6068  ecopovtrn  6139  ecopover  6140  ecopovtrng  6142  ecopoverg  6143  fopwdom  6246  addcanpig  6318  mulcanpig  6319  readdcan  6950  cnegexlem1  6983  addcan  6988  addcan2  6989  neg11  7058  negreb  7072  add20  7264  cru  7386  mulcanapd  7424  uz11  8271  eqreznegel  8325  lbzbi  8327  xneg11  8517  elioc2  8575  elico2  8576  elicc2  8577  fzopth  8694  2ffzeq  8768  frec2uzrand  8872  cj11  9133  sqrt0  9213  bj-peano4  9415  bj-nn0sucALT  9438
  Copyright terms: Public domain W3C validator