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  1597  19.9t  1784  a16gb  1992  sb4b  1996  eupickbi  2211  euor2  2213  2eu1  2225  2eu3  2227  ceqsalg  2814  undif4  3513  sneqbg  3785  opthpr  3792  elpwuni  3991  ordssun  4494  suc11  4498  unizlim  4511  eusv2i  4533  reusv2lem3  4539  reusv3  4544  reuxfr2d  4559  iunpw  4572  ssonprc  4585  onint0  4589  soltmin  5084  ssxpb  5112  xp11  5113  xpcan  5114  xpcan2  5115  iotanul  5236  imadif  5329  2elresin  5357  mpteqb  5616  f1fveq  5788  f1elima  5789  f1imass  5790  fliftf  5816  sorpssuni  6288  sorpssint  6289  oa00  6559  omcan  6569  omopth2  6584  oecan  6589  nnarcl  6616  iserd  6688  ecopover  6764  map0g  6809  fundmen  6936  fopwdom  6972  onfin  7053  fineqvlem  7079  f1finf1o  7088  isfiniteg  7119  inficl  7180  tc00  7435  cardnueq0  7599  cardsdomel  7609  wdomfil  7690  wdomnumr  7693  alephsucdom  7708  cardalephex  7719  dfac12lem2  7772  cfeq0  7884  fin23lem24  7950  fin1a2lem9  8036  carden  8175  axrepnd  8218  axacndlem4  8234  gchpwdom  8298  gchina  8323  r1tskina  8406  addcanpi  8525  mulcanpi  8526  elnpi  8614  addcan  8998  addcan2  8999  neg11  9100  negreb  9114  add20  9288  mulcand  9403  cru  9740  uz11  10252  eqreznegel  10305  lbzbi  10308  rpnnen1  10349  xrmaxlt  10512  xrltmin  10513  xrmaxle  10514  xrlemin  10515  xneg11  10544  xsubge0  10583  xrub  10632  elioc2  10715  elico2  10716  elicc2  10717  fzopth  10830  flidz  10943  expeq0  11134  sq01  11225  fz1eqb  11350  ccatopth  11464  ccatopth2  11465  cj11  11649  sqr0  11729  abs00  11776  recan  11822  rlimdm  12027  rpnnen2  12506  0dvds  12551  dvds1  12579  alzdvds  12580  gcdeq0  12702  algcvgblem  12749  prmexpb  12798  prmreclem3  12967  4sqlem11  13004  moni  13641  spwex  14340  grprcan  14517  grplcan  14536  grpinv11  14539  galcan  14760  sylow2a  14932  subgdisjb  15004  drngmuleq0  15537  lspsncmp  15871  fidomndrng  16050  coe1tm  16351  xrsdsreclb  16420  znidomb  16517  istps2OLD  16661  tgdom  16718  en1top  16724  cmpfi  17137  txcmpb  17340  hmeocnvb  17467  flimcls  17682  hauspwpwf1  17684  flftg  17693  ghmcnp  17799  metrest  18072  icoopnst  18439  iocopnst  18440  ishl2  18789  vitali  18970  mbfi1fseqlem4  19075  aannenlem1  19710  perfect  20472  grporcan  20890  grpolcan  20902  ip2eqi  21437  hial2eq  21687  eigorthi  22419  stge1i  22820  stle0i  22821  mdbr3  22879  mdbr4  22880  atsseq  22929  mdsymlem7  22991  xmulcand  23106  eqvincg  23132  reuxfr3d  23140  untangtr  24062  tfrALTlem  24278  sltval2  24312  ordtopcon  24880  ordtopt0  24883  oooeqim2  25064  prj1b  25090  prj3  25091  fixpb  25104  eqfnung2  25129  efilcp  25563  addcanrg  25678  filnetlem4  26341  seqpo  26468  fphpd  26910  pellexlem3  26927  qirropth  27004  expdioph  27127  rpnnen3  27136  lmisfree  27323  iotasbc  27630  2reu1  27975  2reu3  27977  usgra1v  28137  lshpcmp  29251  lsatcmp  29266  lsatcmp2  29267  ltrneq2  30410  ltrneq  30411  tendospcanN  31286  dochlkr  31648  lcfl7N  31764  hgmap11  32168
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