ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  impbid1 GIF 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  6430  mulcanpig  6431  srpospr  6865  readdcan  7151  cnegexlem1  7184  addcan  7189  addcan2  7190  neg11  7260  negreb  7274  add20  7467  cru  7591  mulcanapd  7640  uz11  8493  eqreznegel  8547  lbzbi  8549  xneg11  8745  elioc2  8803  elico2  8804  elicc2  8805  fzopth  8922  2ffzeq  8996  flqidz  9126  frec2uzrand  9189  cj11  9503  sqrt0  9600  recan  9703  algcvgblem  9886  bj-peano4  10078  bj-nn0sucALT  10101
  Copyright terms: Public domain W3C validator