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

Theorem impbid1 194
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 10 . 2  |-  ( ph  ->  ( ch  ->  ps ) )
41, 3impbid 183 1  |-  ( ph  ->  ( ps  <->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  impbid2  195  iba  489  ibar  490  pm5.71  902  cad0  1390  19.33b  1595  19.9t  1784  sb4b  1993  a16gb  2049  eupickbi  2210  euor2  2212  2eu1  2224  2eu3  2226  ceqsalg  2813  undif4  3512  sneqbg  3784  opthpr  3791  elpwuni  3990  ordssun  4491  suc11  4495  unizlim  4508  eusv2i  4530  reusv2lem3  4536  reusv3  4541  reuxfr2d  4556  iunpw  4569  ssonprc  4582  onint0  4586  soltmin  5081  ssxpb  5109  xp11  5110  xpcan  5111  xpcan2  5112  imadif  5293  2elresin  5321  mpteqb  5576  f1fveq  5748  f1elima  5749  f1imass  5750  fliftf  5776  sorpssuni  6248  sorpssint  6249  iotanul  6268  oa00  6553  omcan  6563  omopth2  6578  oecan  6583  nnarcl  6610  iserd  6682  ecopover  6758  map0g  6803  fundmen  6930  fopwdom  6966  onfin  7047  fineqvlem  7073  f1finf1o  7082  isfiniteg  7113  inficl  7174  tc00  7429  cardnueq0  7593  cardsdomel  7603  wdomfil  7684  wdomnumr  7687  alephsucdom  7702  cardalephex  7713  dfac12lem2  7766  cfeq0  7878  fin23lem24  7944  fin1a2lem9  8030  carden  8169  axrepnd  8212  axacndlem4  8228  gchpwdom  8292  gchina  8317  r1tskina  8400  addcanpi  8519  mulcanpi  8520  elnpi  8608  addcan  8992  addcan2  8993  neg11  9094  negreb  9108  add20  9282  mulcand  9397  cru  9734  uz11  10246  eqreznegel  10299  lbzbi  10302  rpnnen1  10343  xrmaxlt  10506  xrltmin  10507  xrmaxle  10508  xrlemin  10509  xneg11  10538  xsubge0  10577  xrub  10626  elioc2  10709  elico2  10710  elicc2  10711  fzopth  10824  flidz  10937  expeq0  11128  sq01  11219  fz1eqb  11344  ccatopth  11458  ccatopth2  11459  cj11  11643  sqr0  11723  abs00  11770  recan  11816  rlimdm  12021  rpnnen2  12500  0dvds  12545  dvds1  12573  alzdvds  12574  gcdeq0  12696  algcvgblem  12743  prmexpb  12792  prmreclem3  12961  4sqlem11  12998  moni  13635  spwex  14334  grprcan  14511  grplcan  14530  grpinv11  14533  galcan  14754  sylow2a  14926  subgdisjb  14998  drngmuleq0  15531  lspsncmp  15865  fidomndrng  16044  coe1tm  16345  xrsdsreclb  16414  znidomb  16511  istps2OLD  16655  tgdom  16712  en1top  16718  cmpfi  17131  txcmpb  17334  hmeocnvb  17461  flimcls  17676  hauspwpwf1  17678  flftg  17687  ghmcnp  17793  metrest  18066  icoopnst  18433  iocopnst  18434  ishl2  18783  vitali  18964  mbfi1fseqlem4  19069  aannenlem1  19704  perfect  20466  grporcan  20882  grpolcan  20894  ip2eqi  21429  hial2eq  21681  eigorthi  22413  stge1i  22814  stle0i  22815  mdbr3  22873  mdbr4  22874  atsseq  22923  mdsymlem7  22985  untangtr  23467  tfrALTlem  23680  sltval2  23713  ordtopcon  24288  ordtopt0  24291  oooeqim2  24463  prj1b  24489  prj3  24490  fixpb  24503  eqfnung2  24529  efilcp  24963  addcanrg  25078  filnetlem4  25741  seqpo  25868  fphpd  26310  pellexlem3  26327  qirropth  26404  expdioph  26527  rpnnen3  26536  lmisfree  26723  iotasbc  27030  2reu1  27355  2reu3  27357  lshpcmp  28457  lsatcmp  28472  lsatcmp2  28473  ltrneq2  29616  ltrneq  29617  tendospcanN  30492  dochlkr  30854  lcfl7N  30970  hgmap11  31374
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 177
  Copyright terms: Public domain W3C validator