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

Theorem impbid1 141
Description: Infer an equivalence from two implications. (Contributed by NM, 6-Mar-2007.)
Hypotheses
Ref Expression
impbid1.1  |-  ( ph  ->  ( ps  ->  ch ) )
impbid1.2  |-  ( ch 
->  ps )
Assertion
Ref Expression
impbid1  |-  ( ph  ->  ( ps  <->  ch )
)

Proof of Theorem impbid1
StepHypRef Expression
1 impbid1.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
2 impbid1.2 . . 3  |-  ( ch 
->  ps )
32a1i 9 . 2  |-  ( ph  ->  ( ch  ->  ps ) )
41, 3impbid 128 1  |-  ( ph  ->  ( ps  <->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  impbid2  142  iba  298  ibar  299  pm4.81dc  894  pm5.63dc  931  pm4.83dc  936  pm5.71dc  946  19.33b2  1609  19.9t  1622  sb4b  1807  a16gb  1838  euor2  2058  eupickbi  2082  ceqsalg  2717  eqvincg  2812  ddifstab  3212  csbprc  3412  undif4  3429  eqifdc  3510  sssnm  3688  sneqbg  3697  opthpr  3706  elpwuni  3909  exmid01  4128  exmidundif  4136  eusv2i  4383  reusv3  4388  iunpw  4408  suc11g  4479  ssxpbm  4981  ssxp1  4982  ssxp2  4983  xp11m  4984  2elresin  5241  mpteqb  5518  f1fveq  5680  f1elima  5681  f1imass  5682  fliftf  5707  nnsucuniel  6398  iserd  6462  ecopovtrn  6533  ecopover  6534  ecopovtrng  6536  ecopoverg  6537  map0g  6589  fopwdom  6737  f1finf1o  6842  mkvprop  7039  addcanpig  7165  mulcanpig  7166  srpospr  7614  readdcan  7925  cnegexlem1  7960  addcan  7965  addcan2  7966  neg11  8036  negreb  8050  add20  8259  cru  8387  mulcanapd  8445  uz11  9371  eqreznegel  9432  lbzbi  9434  xneg11  9646  xnn0xadd0  9679  xsubge0  9693  elioc2  9748  elico2  9749  elicc2  9750  fzopth  9871  2ffzeq  9948  flqidz  10089  addmodlteq  10201  frec2uzrand  10208  expcan  10493  nn0opthd  10499  fz1eqb  10568  cj11  10708  sqrt0  10807  recan  10912  0dvds  11547  dvds1  11585  alzdvds  11586  nn0enne  11633  nn0oddm1d2  11640  nnoddm1d2  11641  divalgmod  11658  gcdeq0  11699  algcvgblem  11764  prmexpb  11863  ennnfonelemim  11971  tgdom  12278  en1top  12283  hmeocnvb  12524  metrest  12712  bj-nnbist  13122  bj-nnbidc  13131  bj-peano4  13322  bj-nn0sucALT  13345
  Copyright terms: Public domain W3C validator