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

Theorem impbid1 207
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 194 1  |-  ( ph  ->  ( ps  <->  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 189
This theorem is referenced by:  impbid2  208  iba  506  ibar  507  pm5.71  945  cad0  1516  19.33b  1741  19.40b  1743  19.9t  1943  19.9tOLD  1946  axc16gb  1999  equs5  2146  sb4b  2152  2eu1  2351  2eu1OLD  2352  2eu3  2354  ceqsalgALT  3108  csbprc  3799  undif4  3850  sneqbg  4168  opthpr  4176  elpwuni  4388  eusv2i  4619  reusv2lem3  4625  reusv3  4630  reuxfr2d  4642  soltmin  5253  ssxpb  5288  xp11  5289  xpcan  5290  xpcan2  5291  ordssun  5539  suc11  5543  unizlim  5556  iotanul  5578  imadif  5674  2elresin  5703  mpteqb  5978  f1fveq  6176  f1elima  6177  f1imass  6178  fliftf  6221  sorpssuni  6592  sorpssint  6593  iunpw  6617  ssonprc  6631  onint0  6635  oa00  7266  omcan  7276  omopth2  7291  oecan  7296  nnarcl  7323  iserd  7395  ecopover  7473  map0g  7517  fundmen  7648  fopwdom  7684  onfin  7767  fineqvlem  7790  f1finf1o  7802  isfiniteg  7835  inficl  7943  tc00  8235  cardnueq0  8401  cardsdomel  8411  wdomfil  8494  wdomnumr  8497  alephsucdom  8512  cardalephex  8523  dfac12lem2  8576  cfeq0  8688  fin23lem24  8754  fin1a2lem9  8840  carden  8978  axrepnd  9021  axacndlem4  9037  gchpwdom  9097  gchina  9126  r1tskina  9209  addcanpi  9326  mulcanpi  9327  elnpi  9415  addcan  9819  addcan2  9820  neg11  9927  negreb  9941  add20  10128  mulcand  10247  cru  10603  nn0lt10b  11000  uz11  11183  eqreznegel  11251  lbzbi  11254  rpnnen1  11297  xrmaxlt  11478  xrltmin  11479  xrmaxle  11480  xrlemin  11481  xneg11  11510  xsubge0  11549  xrub  11599  elioc2  11699  elico2  11700  elicc2  11701  fzopth  11837  2ffzeq  11912  flidz  12047  expeq0  12303  sq01  12395  fz1eqb  12537  hashen1  12551  hash1snb  12592  wrdnval  12695  eqwrd  12706  wrdl1s1  12747  ccatopth  12822  ccatopth2  12823  wrdlen2  13017  cj11  13219  sqrt0  13299  abs00  13346  recan  13393  rlimdm  13608  rpnnen2  14271  0dvds  14316  dvds1  14346  alzdvds  14348  gcdeq0  14478  algcvgblem  14529  prmexpb  14663  prmreclem3  14855  4sqlem11  14892  moni  15634  grprcan  16692  grplcan  16711  grpinv11  16716  galcan  16951  sylow2a  17264  subgdisjb  17336  drngmuleq0  17991  lspsncmp  18332  fidomndrng  18524  coe1tm  18859  xrsdsreclb  19008  znidomb  19124  lmisfree  19392  tgdom  19986  en1top  19992  cmpfi  20415  txcmpb  20651  hmeocnvb  20781  flimcls  20992  hauspwpwf1  20994  flftg  21003  ghmcnp  21121  metrest  21531  icoopnst  21959  iocopnst  21960  ishl2  22329  vitali  22563  mbfi1fseqlem4  22668  aannenlem1  23276  perfect  24151  usgra1v  25109  is2wlk  25287  usgra2wlkspth  25341  usg2wotspth  25604  usg2spot2nb  25785  extwwlkfab  25810  grporcan  25941  grpolcan  25953  ip2eqi  26490  hial2eq  26751  eigorthi  27482  stge1i  27883  stle0i  27884  mdbr3  27942  mdbr4  27943  atsseq  27992  mdsymlem7  28054  eqvincg  28100  reuxfr3d  28117  disjunsn  28200  fpwrelmapffslem  28317  xmulcand  28391  prsdm  28722  prsrn  28723  mthmpps  30222  untangtr  30343  sltval2  30544  filnetlem4  31036  ordtopcon  31098  ordtopt0  31101  bj-dfbi6  31150  bj-19.9htbi  31251  bj-axc16gb  31318  bj-equs5v  31325  bj-sb4bv  31331  icorempt2  31701  wl-lem-moexsb  31817  seqpo  31996  lshpcmp  32479  lsatcmp  32494  lsatcmp2  32495  ltrneq2  33638  ltrneq  33639  tendospcanN  34516  dochlkr  34878  lcfl7N  34994  hgmap11  35398  fphpd  35584  pellexlem3  35601  qirropth  35682  expdioph  35804  rpnnen3  35813  iotasbc  36634  2reu1  38326  2reu3  38328  rlimdmafv  38397  evenprm2  38560  perfectALTV  38563  nnsum3primesle9  38607  funop1  38725  fzoopth  38758  2ffzoeq  38759  usgrausgrb  38890  usgra2pthspth  38969  0ringdif  39174  islinindfis  39548  lincresunit3lem3  39573  nn0enne  39632  blen1b  39705
  Copyright terms: Public domain W3C validator