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  1598  19.9t  1794  a16gb  2003  sb4b  2007  eupickbi  2222  euor2  2224  2eu1  2236  2eu3  2238  ceqsalg  2825  undif4  3524  sneqbg  3799  opthpr  3806  elpwuni  4005  ordssun  4508  suc11  4512  unizlim  4525  eusv2i  4547  reusv2lem3  4553  reusv3  4558  reuxfr2d  4573  iunpw  4586  ssonprc  4599  onint0  4603  soltmin  5098  ssxpb  5126  xp11  5127  xpcan  5128  xpcan2  5129  iotanul  5250  imadif  5343  2elresin  5371  mpteqb  5630  f1fveq  5802  f1elima  5803  f1imass  5804  fliftf  5830  sorpssuni  6302  sorpssint  6303  oa00  6573  omcan  6583  omopth2  6598  oecan  6603  nnarcl  6630  iserd  6702  ecopover  6778  map0g  6823  fundmen  6950  fopwdom  6986  onfin  7067  fineqvlem  7093  f1finf1o  7102  isfiniteg  7133  inficl  7194  tc00  7449  cardnueq0  7613  cardsdomel  7623  wdomfil  7704  wdomnumr  7707  alephsucdom  7722  cardalephex  7733  dfac12lem2  7786  cfeq0  7898  fin23lem24  7964  fin1a2lem9  8050  carden  8189  axrepnd  8232  axacndlem4  8248  gchpwdom  8312  gchina  8337  r1tskina  8420  addcanpi  8539  mulcanpi  8540  elnpi  8628  addcan  9012  addcan2  9013  neg11  9114  negreb  9128  add20  9302  mulcand  9417  cru  9754  uz11  10266  eqreznegel  10319  lbzbi  10322  rpnnen1  10363  xrmaxlt  10526  xrltmin  10527  xrmaxle  10528  xrlemin  10529  xneg11  10558  xsubge0  10597  xrub  10646  elioc2  10729  elico2  10730  elicc2  10731  fzopth  10844  flidz  10957  expeq0  11148  sq01  11239  fz1eqb  11364  ccatopth  11478  ccatopth2  11479  cj11  11663  sqr0  11743  abs00  11790  recan  11836  rlimdm  12041  rpnnen2  12520  0dvds  12565  dvds1  12593  alzdvds  12594  gcdeq0  12716  algcvgblem  12763  prmexpb  12812  prmreclem3  12981  4sqlem11  13018  moni  13655  spwex  14354  grprcan  14531  grplcan  14550  grpinv11  14553  galcan  14774  sylow2a  14946  subgdisjb  15018  drngmuleq0  15551  lspsncmp  15885  fidomndrng  16064  coe1tm  16365  xrsdsreclb  16434  znidomb  16531  istps2OLD  16675  tgdom  16732  en1top  16738  cmpfi  17151  txcmpb  17354  hmeocnvb  17481  flimcls  17696  hauspwpwf1  17698  flftg  17707  ghmcnp  17813  metrest  18086  icoopnst  18453  iocopnst  18454  ishl2  18803  vitali  18984  mbfi1fseqlem4  19089  aannenlem1  19724  perfect  20486  grporcan  20904  grpolcan  20916  ip2eqi  21451  hial2eq  21701  eigorthi  22433  stge1i  22834  stle0i  22835  mdbr3  22893  mdbr4  22894  atsseq  22943  mdsymlem7  23005  xmulcand  23120  eqvincg  23146  reuxfr3d  23154  untangtr  24075  tfrALTlem  24347  sltval2  24381  ordtopcon  24950  ordtopt0  24953  oooeqim2  25156  prj1b  25182  prj3  25183  fixpb  25196  eqfnung2  25221  efilcp  25655  addcanrg  25770  filnetlem4  26433  seqpo  26560  fphpd  27002  pellexlem3  27019  qirropth  27096  expdioph  27219  rpnnen3  27228  lmisfree  27415  iotasbc  27722  2reu1  28067  2reu3  28069  rlimdmafv  28145  usgra1v  28260  equs5bAUX7  29510  a16gbNEW7  29522  sb4bNEW7  29528  lshpcmp  29800  lsatcmp  29815  lsatcmp2  29816  ltrneq2  30959  ltrneq  30960  tendospcanN  31835  dochlkr  32197  lcfl7N  32313  hgmap11  32717
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