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

Theorem impbid1 195
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 184 1  |-  ( ph  ->  ( ps  <->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  impbid2  196  iba  490  ibar  491  pm5.71  903  cad0  1406  19.33b  1615  19.9t  1789  19.9tOLD  1876  a16gb  2099  sb4b  2103  eupickbi  2320  euor2  2322  2eu1  2334  2eu3  2336  ceqsalg  2940  undif4  3644  sneqbg  3929  opthpr  3936  elpwuni  4138  ordssun  4640  suc11  4644  unizlim  4657  eusv2i  4679  reusv2lem3  4685  reusv3  4690  reuxfr2d  4705  iunpw  4718  ssonprc  4731  onint0  4735  soltmin  5232  ssxpb  5262  xp11  5263  xpcan  5264  xpcan2  5265  iotanul  5392  imadif  5487  2elresin  5515  mpteqb  5778  f1fveq  5967  f1elima  5968  f1imass  5969  fliftf  5996  sorpssuni  6490  sorpssint  6491  oa00  6761  omcan  6771  omopth2  6786  oecan  6791  nnarcl  6818  iserd  6890  ecopover  6967  map0g  7012  fundmen  7139  fopwdom  7175  onfin  7256  fineqvlem  7282  f1finf1o  7294  isfiniteg  7326  inficl  7388  tc00  7643  cardnueq0  7807  cardsdomel  7817  wdomfil  7898  wdomnumr  7901  alephsucdom  7916  cardalephex  7927  dfac12lem2  7980  cfeq0  8092  fin23lem24  8158  fin1a2lem9  8244  carden  8382  axrepnd  8425  axacndlem4  8441  gchpwdom  8505  gchina  8530  r1tskina  8613  addcanpi  8732  mulcanpi  8733  elnpi  8821  addcan  9206  addcan2  9207  neg11  9308  negreb  9322  add20  9496  mulcand  9611  cru  9948  uz11  10464  eqreznegel  10517  lbzbi  10520  rpnnen1  10561  xrmaxlt  10725  xrltmin  10726  xrmaxle  10727  xrlemin  10728  xneg11  10757  xsubge0  10796  xrub  10846  elioc2  10929  elico2  10930  elicc2  10931  fzopth  11045  flidz  11173  expeq0  11365  sq01  11456  fz1eqb  11592  hash1snb  11636  ccatopth  11731  ccatopth2  11732  cj11  11922  sqr0  12002  abs00  12049  recan  12095  rlimdm  12300  rpnnen2  12780  0dvds  12825  dvds1  12853  alzdvds  12854  gcdeq0  12976  algcvgblem  13023  prmexpb  13072  prmreclem3  13241  4sqlem11  13278  moni  13917  spwex  14616  grprcan  14793  grplcan  14812  grpinv11  14815  galcan  15036  sylow2a  15208  subgdisjb  15280  drngmuleq0  15813  lspsncmp  16143  fidomndrng  16322  coe1tm  16620  xrsdsreclb  16700  znidomb  16797  istps2OLD  16941  tgdom  16998  en1top  17004  cmpfi  17425  txcmpb  17629  hmeocnvb  17759  flimcls  17970  hauspwpwf1  17972  flftg  17981  ghmcnp  18097  metrest  18507  icoopnst  18917  iocopnst  18918  ishl2  19277  vitali  19458  mbfi1fseqlem4  19563  aannenlem1  20198  perfect  20968  usgra1v  21362  is2wlk  21518  grporcan  21762  grpolcan  21774  ip2eqi  22311  hial2eq  22561  eigorthi  23293  stge1i  23694  stle0i  23695  mdbr3  23753  mdbr4  23754  atsseq  23803  mdsymlem7  23865  eqvincg  23914  reuxfr3d  23929  xmulcand  24120  untangtr  25116  tfrALTlem  25490  sltval2  25524  ordtopcon  26093  ordtopt0  26096  filnetlem4  26300  seqpo  26341  fphpd  26767  pellexlem3  26784  qirropth  26861  expdioph  26984  rpnnen3  26993  lmisfree  27180  iotasbc  27487  2reu1  27831  2reu3  27833  rlimdmafv  27908  usgra2pthspth  28035  usgra2wlkspth  28038  usg2wotspth  28081  usg2spot2nb  28168  equs5bAUX7  29239  a16gbNEW7  29251  sb4bNEW7  29257  lshpcmp  29471  lsatcmp  29486  lsatcmp2  29487  ltrneq2  30630  ltrneq  30631  tendospcanN  31506  dochlkr  31868  lcfl7N  31984  hgmap11  32388
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 178
  Copyright terms: Public domain W3C validator