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

Theorem impbid1 196
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 185 1  |-  ( ph  ->  ( ps  <->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178
This theorem is referenced by:  impbid2  197  iba  491  ibar  492  pm5.71  904  cad0  1410  19.33b  1619  19.9t  1794  19.9tOLD  1881  a16gb  2053  sb4b  2095  eupickbi  2348  euor2  2350  2eu1  2362  2eu3  2364  ceqsalg  2981  undif4  3685  sneqbg  3970  opthpr  3977  elpwuni  4179  ordssun  4682  suc11  4686  unizlim  4699  eusv2i  4721  reusv2lem3  4727  reusv3  4732  reuxfr2d  4747  iunpw  4760  ssonprc  4773  onint0  4777  soltmin  5274  ssxpb  5304  xp11  5305  xpcan  5306  xpcan2  5307  iotanul  5434  imadif  5529  2elresin  5557  mpteqb  5820  f1fveq  6009  f1elima  6010  f1imass  6011  fliftf  6038  sorpssuni  6532  sorpssint  6533  oa00  6803  omcan  6813  omopth2  6828  oecan  6833  nnarcl  6860  iserd  6932  ecopover  7009  map0g  7054  fundmen  7181  fopwdom  7217  onfin  7298  fineqvlem  7324  f1finf1o  7336  isfiniteg  7368  inficl  7431  tc00  7688  cardnueq0  7852  cardsdomel  7862  wdomfil  7943  wdomnumr  7946  alephsucdom  7961  cardalephex  7972  dfac12lem2  8025  cfeq0  8137  fin23lem24  8203  fin1a2lem9  8289  carden  8427  axrepnd  8470  axacndlem4  8486  gchpwdom  8550  gchina  8575  r1tskina  8658  addcanpi  8777  mulcanpi  8778  elnpi  8866  addcan  9251  addcan2  9252  neg11  9353  negreb  9367  add20  9541  mulcand  9656  cru  9993  uz11  10509  eqreznegel  10562  lbzbi  10565  rpnnen1  10606  xrmaxlt  10770  xrltmin  10771  xrmaxle  10772  xrlemin  10773  xneg11  10802  xsubge0  10841  xrub  10891  elioc2  10974  elico2  10975  elicc2  10976  fzopth  11090  flidz  11219  expeq0  11411  sq01  11502  fz1eqb  11638  hash1snb  11682  ccatopth  11777  ccatopth2  11778  cj11  11968  sqr0  12048  abs00  12095  recan  12141  rlimdm  12346  rpnnen2  12826  0dvds  12871  dvds1  12899  alzdvds  12900  gcdeq0  13022  algcvgblem  13069  prmexpb  13118  prmreclem3  13287  4sqlem11  13324  moni  13963  spwex  14662  grprcan  14839  grplcan  14858  grpinv11  14861  galcan  15082  sylow2a  15254  subgdisjb  15326  drngmuleq0  15859  lspsncmp  16189  fidomndrng  16368  coe1tm  16666  xrsdsreclb  16746  znidomb  16843  istps2OLD  16987  tgdom  17044  en1top  17050  cmpfi  17472  txcmpb  17677  hmeocnvb  17807  flimcls  18018  hauspwpwf1  18020  flftg  18029  ghmcnp  18145  metrest  18555  icoopnst  18965  iocopnst  18966  ishl2  19325  vitali  19506  mbfi1fseqlem4  19611  aannenlem1  20246  perfect  21016  usgra1v  21410  is2wlk  21566  grporcan  21810  grpolcan  21822  ip2eqi  22359  hial2eq  22609  eigorthi  23341  stge1i  23742  stle0i  23743  mdbr3  23801  mdbr4  23802  atsseq  23851  mdsymlem7  23913  eqvincg  23962  reuxfr3d  23977  xmulcand  24168  untangtr  25164  sltval2  25612  ordtopcon  26190  ordtopt0  26193  filnetlem4  26411  seqpo  26452  fphpd  26878  pellexlem3  26895  qirropth  26972  expdioph  27095  rpnnen3  27104  lmisfree  27290  iotasbc  27597  2reu1  27941  2reu3  27943  rlimdmafv  28018  2ffzeq  28122  fzoopth  28140  2ffzoeq  28141  wrdeq0  28173  usgra2pthspth  28306  usgra2wlkspth  28309  usg2wotspth  28352  usg2spot2nb  28455  equs5bAUX7  29536  a16gbNEW7  29548  sb4bNEW7  29554  lshpcmp  29787  lsatcmp  29802  lsatcmp2  29803  ltrneq2  30946  ltrneq  30947  tendospcanN  31822  dochlkr  32184  lcfl7N  32300  hgmap11  32704
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator