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  1442  19.33b  1663  19.9t  1823  ax16gb  2015  equs5  2042  sb4b  2048  euor2OLD  2311  eupickbiOLD  2345  2eu1  2361  2eu3  2363  ceqsalgALT  2993  csbprc  3668  undif4  3730  sneqbg  4038  opthpr  4045  elpwuni  4253  eusv2i  4484  reusv2lem3  4490  reusv3  4495  reuxfr2d  4510  ordssun  4813  suc11  4817  unizlim  4830  soltmin  5232  ssxpb  5267  xp11  5268  xpcan  5269  xpcan2  5270  iotanul  5391  imadif  5488  2elresin  5517  mpteqb  5783  f1fveq  5970  f1elima  5971  f1imass  5972  fliftf  6003  sorpssuni  6364  sorpssint  6365  iunpw  6385  ssonprc  6398  onint0  6402  oa00  6990  omcan  7000  omopth2  7015  oecan  7020  nnarcl  7047  iserd  7119  ecopover  7196  map0g  7244  fundmen  7375  fopwdom  7411  onfin  7493  fineqvlem  7519  f1finf1o  7531  isfiniteg  7564  inficl  7667  tc00  7960  cardnueq0  8126  cardsdomel  8136  wdomfil  8223  wdomnumr  8226  alephsucdom  8241  cardalephex  8252  dfac12lem2  8305  cfeq0  8417  fin23lem24  8483  fin1a2lem9  8569  carden  8707  axrepnd  8750  axacndlem4  8769  gchpwdom  8829  gchina  8858  r1tskina  8941  addcanpi  9060  mulcanpi  9061  elnpi  9149  addcan  9545  addcan2  9546  neg11  9652  negreb  9666  add20  9843  mulcand  9961  cru  10306  uz11  10875  eqreznegel  10932  lbzbi  10935  rpnnen1  10976  xrmaxlt  11145  xrltmin  11146  xrmaxle  11147  xrlemin  11148  xneg11  11177  xsubge0  11216  xrub  11266  elioc2  11350  elico2  11351  elicc2  11352  fzopth  11487  flidz  11651  expeq0  11886  sq01  11978  fz1eqb  12116  hash1snb  12163  eqwrd  12257  wrdl1s1  12293  ccatopth  12356  ccatopth2  12357  wrdlen2  12540  cj11  12643  sqr0  12723  abs00  12770  recan  12816  rlimdm  13021  rpnnen2  13500  0dvds  13545  dvds1  13573  alzdvds  13575  gcdeq0  13697  algcvgblem  13744  prmexpb  13795  prmreclem3  13971  4sqlem11  14008  moni  14667  grprcan  15562  grplcan  15581  grpinv11  15586  galcan  15813  sylow2a  16109  subgdisjb  16181  drngmuleq0  16833  lspsncmp  17174  fidomndrng  17356  coe1tm  17701  xrsdsreclb  17835  znidomb  17969  lmisfree  18246  istps2OLD  18501  tgdom  18558  en1top  18564  cmpfi  18986  txcmpb  19192  hmeocnvb  19322  flimcls  19533  hauspwpwf1  19535  flftg  19544  ghmcnp  19660  metrest  20074  icoopnst  20486  iocopnst  20487  ishl2  20857  vitali  21068  mbfi1fseqlem4  21171  aannenlem1  21769  perfect  22545  usgra1v  23259  is2wlk  23415  grporcan  23659  grpolcan  23671  ip2eqi  24208  hial2eq  24459  eigorthi  25192  stge1i  25593  stle0i  25594  mdbr3  25652  mdbr4  25653  atsseq  25702  mdsymlem7  25764  eqvincg  25810  reuxfr3d  25824  xmulcand  26047  untangtr  27316  sltval2  27748  ordtopcon  28237  ordtopt0  28240  wl-sb6nae  28333  wl-lem-moexsb  28344  filnetlem4  28555  seqpo  28596  fphpd  29108  pellexlem3  29125  qirropth  29202  expdioph  29325  rpnnen3  29334  iotasbc  29626  2reu1  29963  2reu3  29965  rlimdmafv  30036  2ffzeq  30157  fzoopth  30166  2ffzoeq  30167  usgra2pthspth  30248  usgra2wlkspth  30251  usg2wotspth  30356  wrdnval  30427  usg2spot2nb  30611  extwwlkfab  30636  hashen1  30689  islinindfis  30872  lincresunit3lem3  30897  bj-dfbi6  31964  bj-19.40b  32041  bj-ax16gb  32117  bj-equs5v  32124  bj-sb4bv  32130  lshpcmp  32473  lsatcmp  32488  lsatcmp2  32489  ltrneq2  33632  ltrneq  33633  tendospcanN  34508  dochlkr  34870  lcfl7N  34986  hgmap11  35390
  Copyright terms: Public domain W3C validator