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  503  ibar  504  pm5.71  927  cad0  1443  19.33b  1664  19.9t  1829  ax16gb  1880  equs5  2052  sb4b  2058  euor2OLD  2322  eupickbiOLD  2356  2eu1  2373  2eu1OLD  2374  2eu3  2376  ceqsalgALT  3102  csbprc  3780  undif4  3842  sneqbg  4150  opthpr  4157  elpwuni  4365  eusv2i  4596  reusv2lem3  4602  reusv3  4607  reuxfr2d  4622  ordssun  4925  suc11  4929  unizlim  4942  soltmin  5344  ssxpb  5379  xp11  5380  xpcan  5381  xpcan2  5382  iotanul  5503  imadif  5600  2elresin  5629  mpteqb  5896  f1fveq  6083  f1elima  6084  f1imass  6085  fliftf  6116  sorpssuni  6478  sorpssint  6479  iunpw  6499  ssonprc  6512  onint0  6516  oa00  7107  omcan  7117  omopth2  7132  oecan  7137  nnarcl  7164  iserd  7236  ecopover  7313  map0g  7361  fundmen  7492  fopwdom  7528  onfin  7611  fineqvlem  7637  f1finf1o  7649  isfiniteg  7682  inficl  7785  tc00  8078  cardnueq0  8244  cardsdomel  8254  wdomfil  8341  wdomnumr  8344  alephsucdom  8359  cardalephex  8370  dfac12lem2  8423  cfeq0  8535  fin23lem24  8601  fin1a2lem9  8687  carden  8825  axrepnd  8868  axacndlem4  8887  gchpwdom  8947  gchina  8976  r1tskina  9059  addcanpi  9178  mulcanpi  9179  elnpi  9267  addcan  9663  addcan2  9664  neg11  9770  negreb  9784  add20  9961  mulcand  10079  cru  10424  uz11  10993  eqreznegel  11050  lbzbi  11053  rpnnen1  11094  xrmaxlt  11263  xrltmin  11264  xrmaxle  11265  xrlemin  11266  xneg11  11295  xsubge0  11334  xrub  11384  elioc2  11468  elico2  11469  elicc2  11470  fzopth  11611  flidz  11775  expeq0  12010  sq01  12102  fz1eqb  12240  hashen1  12253  hash1snb  12288  eqwrd  12382  wrdl1s1  12418  ccatopth  12481  ccatopth2  12482  wrdlen2  12665  cj11  12768  sqr0  12848  abs00  12895  recan  12941  rlimdm  13146  rpnnen2  13625  0dvds  13670  dvds1  13698  alzdvds  13700  gcdeq0  13822  algcvgblem  13869  prmexpb  13920  prmreclem3  14096  4sqlem11  14133  moni  14793  grprcan  15689  grplcan  15708  grpinv11  15713  galcan  15940  sylow2a  16238  subgdisjb  16310  drngmuleq0  16977  lspsncmp  17319  fidomndrng  17501  coe1tm  17849  xrsdsreclb  17984  znidomb  18118  lmisfree  18395  istps2OLD  18657  tgdom  18714  en1top  18720  cmpfi  19142  txcmpb  19348  hmeocnvb  19478  flimcls  19689  hauspwpwf1  19691  flftg  19700  ghmcnp  19816  metrest  20230  icoopnst  20642  iocopnst  20643  ishl2  21013  vitali  21225  mbfi1fseqlem4  21328  aannenlem1  21926  perfect  22702  usgra1v  23459  is2wlk  23615  grporcan  23859  grpolcan  23871  ip2eqi  24408  hial2eq  24659  eigorthi  25392  stge1i  25793  stle0i  25794  mdbr3  25852  mdbr4  25853  atsseq  25902  mdsymlem7  25964  eqvincg  26010  reuxfr3d  26024  xmulcand  26240  untangtr  27508  sltval2  27940  ordtopcon  28428  ordtopt0  28431  wl-sb6nae  28529  wl-lem-moexsb  28540  filnetlem4  28749  seqpo  28790  fphpd  29302  pellexlem3  29319  qirropth  29396  expdioph  29519  rpnnen3  29528  iotasbc  29820  2reu1  30157  2reu3  30159  rlimdmafv  30230  2ffzeq  30351  fzoopth  30360  2ffzoeq  30361  usgra2pthspth  30442  usgra2wlkspth  30445  usg2wotspth  30550  wrdnval  30621  usg2spot2nb  30805  extwwlkfab  30830  islinindfis  31101  lincresunit3lem3  31126  bj-dfbi6  32396  bj-19.40b  32479  bj-19.9htbi  32510  bj-ax16gb  32577  bj-equs5v  32584  bj-sb4bv  32590  lshpcmp  32956  lsatcmp  32971  lsatcmp2  32972  ltrneq2  34115  ltrneq  34116  tendospcanN  34991  dochlkr  35353  lcfl7N  35469  hgmap11  35873
  Copyright terms: Public domain W3C validator