MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  impbid1 Structured version   Unicode version

Theorem impbid1 203
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 11 . 2  |-  ( ph  ->  ( ch  ->  ps ) )
41, 3impbid 191 1  |-  ( ph  ->  ( ps  <->  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185
This theorem is referenced by:  impbid2  204  iba  500  ibar  501  pm5.71  920  cad0  1445  19.33b  1662  19.9t  1822  ax16gb  2013  equs5  2041  sb4b  2047  euor2OLD  2308  eupickbiOLD  2343  2eu1  2358  2eu3  2360  ceqsalg  2987  csbprc  3661  undif4  3723  sneqbg  4031  opthpr  4038  elpwuni  4246  eusv2i  4477  reusv2lem3  4483  reusv3  4488  reuxfr2d  4503  ordssun  4805  suc11  4809  unizlim  4822  soltmin  5225  ssxpb  5260  xp11  5261  xpcan  5262  xpcan2  5263  iotanul  5384  imadif  5481  2elresin  5510  mpteqb  5776  f1fveq  5962  f1elima  5963  f1imass  5964  fliftf  5995  sorpssuni  6358  sorpssint  6359  iunpw  6379  ssonprc  6392  onint0  6396  oa00  6986  omcan  6996  omopth2  7011  oecan  7016  nnarcl  7043  iserd  7115  ecopover  7192  map0g  7240  fundmen  7371  fopwdom  7407  onfin  7489  fineqvlem  7515  f1finf1o  7527  isfiniteg  7560  inficl  7663  tc00  7956  cardnueq0  8122  cardsdomel  8132  wdomfil  8219  wdomnumr  8222  alephsucdom  8237  cardalephex  8248  dfac12lem2  8301  cfeq0  8413  fin23lem24  8479  fin1a2lem9  8565  carden  8703  axrepnd  8746  axacndlem4  8765  gchpwdom  8825  gchina  8854  r1tskina  8937  addcanpi  9056  mulcanpi  9057  elnpi  9145  addcan  9541  addcan2  9542  neg11  9648  negreb  9662  add20  9839  mulcand  9957  cru  10302  uz11  10871  eqreznegel  10928  lbzbi  10931  rpnnen1  10972  xrmaxlt  11141  xrltmin  11142  xrmaxle  11143  xrlemin  11144  xneg11  11173  xsubge0  11212  xrub  11262  elioc2  11346  elico2  11347  elicc2  11348  fzopth  11482  flidz  11643  expeq0  11878  sq01  11970  fz1eqb  12108  hash1snb  12155  eqwrd  12249  wrdl1s1  12285  ccatopth  12348  ccatopth2  12349  wrdlen2  12532  cj11  12635  sqr0  12715  abs00  12762  recan  12808  rlimdm  13013  rpnnen2  13491  0dvds  13536  dvds1  13564  alzdvds  13566  gcdeq0  13688  algcvgblem  13735  prmexpb  13786  prmreclem3  13962  4sqlem11  13999  moni  14658  grprcan  15551  grplcan  15570  grpinv11  15575  galcan  15802  sylow2a  16098  subgdisjb  16170  drngmuleq0  16779  lspsncmp  17119  fidomndrng  17301  coe1tm  17624  xrsdsreclb  17704  znidomb  17836  lmisfree  18113  istps2OLD  18368  tgdom  18425  en1top  18431  cmpfi  18853  txcmpb  19059  hmeocnvb  19189  flimcls  19400  hauspwpwf1  19402  flftg  19411  ghmcnp  19527  metrest  19941  icoopnst  20353  iocopnst  20354  ishl2  20724  vitali  20935  mbfi1fseqlem4  21038  aannenlem1  21679  perfect  22455  usgra1v  23131  is2wlk  23287  grporcan  23531  grpolcan  23543  ip2eqi  24080  hial2eq  24331  eigorthi  25064  stge1i  25465  stle0i  25466  mdbr3  25524  mdbr4  25525  atsseq  25574  mdsymlem7  25636  eqvincg  25682  reuxfr3d  25697  xmulcand  25919  untangtr  27212  sltval2  27644  ordtopcon  28133  ordtopt0  28136  wl-sb6nae  28230  filnetlem4  28446  seqpo  28487  fphpd  29000  pellexlem3  29017  qirropth  29094  expdioph  29217  rpnnen3  29226  iotasbc  29518  2reu1  29856  2reu3  29858  rlimdmafv  29929  2ffzeq  30050  fzoopth  30059  2ffzoeq  30060  usgra2pthspth  30141  usgra2wlkspth  30144  usg2wotspth  30249  wrdnval  30320  usg2spot2nb  30504  extwwlkfab  30529  hashen1  30582  islinindfis  30713  lincresunit3lem3  30738  bj-19.40b  31844  bj-ax16gb  31912  bj-equs5v  31918  bj-sb4bv  31924  lshpcmp  32227  lsatcmp  32242  lsatcmp2  32243  ltrneq2  33386  ltrneq  33387  tendospcanN  34262  dochlkr  34624  lcfl7N  34740  hgmap11  35144
  Copyright terms: Public domain W3C validator