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

Theorem impbid1 203
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 191 1  |-  ( ph  ->  ( ps  <->  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
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 185
This theorem is referenced by:  impbid2  204  iba  503  ibar  504  pm5.71  934  cad0  1453  19.33b  1681  19.40b  1683  19.9t  1874  ax16gb  1926  equs5  2076  sb4b  2082  2eu1  2360  2eu1OLD  2361  2eu3  2363  ceqsalgALT  3119  csbprc  3803  undif4  3865  sneqbg  4181  opthpr  4189  elpwuni  4399  eusv2i  4630  reusv2lem3  4636  reusv3  4641  reuxfr2d  4656  ordssun  4963  suc11  4967  unizlim  4980  soltmin  5392  ssxpb  5427  xp11  5428  xpcan  5429  xpcan2  5430  iotanul  5552  imadif  5649  2elresin  5678  mpteqb  5951  f1fveq  6151  f1elima  6152  f1imass  6153  fliftf  6194  sorpssuni  6570  sorpssint  6571  iunpw  6595  ssonprc  6608  onint0  6612  oa00  7206  omcan  7216  omopth2  7231  oecan  7236  nnarcl  7263  iserd  7335  ecopover  7413  map0g  7456  fundmen  7587  fopwdom  7623  onfin  7706  fineqvlem  7732  f1finf1o  7744  isfiniteg  7778  inficl  7883  tc00  8177  cardnueq0  8343  cardsdomel  8353  wdomfil  8440  wdomnumr  8443  alephsucdom  8458  cardalephex  8469  dfac12lem2  8522  cfeq0  8634  fin23lem24  8700  fin1a2lem9  8786  carden  8924  axrepnd  8967  axacndlem4  8986  gchpwdom  9046  gchina  9075  r1tskina  9158  addcanpi  9275  mulcanpi  9276  elnpi  9364  addcan  9762  addcan2  9763  neg11  9870  negreb  9884  add20  10065  mulcand  10183  cru  10529  nn0lt10b  10927  uz11  11107  eqreznegel  11171  lbzbi  11174  rpnnen1  11217  xrmaxlt  11386  xrltmin  11387  xrmaxle  11388  xrlemin  11389  xneg11  11418  xsubge0  11457  xrub  11507  elioc2  11591  elico2  11592  elicc2  11593  fzopth  11724  2ffzeq  11797  flidz  11921  expeq0  12170  sq01  12262  fz1eqb  12400  hashen1  12413  hash1snb  12453  wrdnval  12545  eqwrd  12556  wrdl1s1  12596  ccatopth  12669  ccatopth2  12670  wrdlen2  12860  cj11  12969  sqrt0  13049  abs00  13096  recan  13143  rlimdm  13348  rpnnen2  13831  0dvds  13876  dvds1  13906  alzdvds  13908  gcdeq0  14031  algcvgblem  14078  prmexpb  14130  prmreclem3  14308  4sqlem11  14345  moni  15003  grprcan  15952  grplcan  15971  grpinv11  15976  galcan  16211  sylow2a  16508  subgdisjb  16580  drngmuleq0  17287  lspsncmp  17630  fidomndrng  17824  coe1tm  18182  xrsdsreclb  18333  znidomb  18467  lmisfree  18744  istps2OLD  19289  tgdom  19346  en1top  19352  cmpfi  19774  txcmpb  20011  hmeocnvb  20141  flimcls  20352  hauspwpwf1  20354  flftg  20363  ghmcnp  20479  metrest  20893  icoopnst  21305  iocopnst  21306  ishl2  21676  vitali  21888  mbfi1fseqlem4  21991  aannenlem1  22589  perfect  23371  usgra1v  24255  is2wlk  24432  usgra2wlkspth  24486  usg2wotspth  24749  usg2spot2nb  24930  extwwlkfab  24955  grporcan  25088  grpolcan  25100  ip2eqi  25637  hial2eq  25888  eigorthi  26621  stge1i  27022  stle0i  27023  mdbr3  27081  mdbr4  27082  atsseq  27131  mdsymlem7  27193  eqvincg  27239  reuxfr3d  27253  disjunsn  27318  fpwrelmapffslem  27420  xmulcand  27483  prsdm  27762  prsrn  27763  mthmpps  28808  untangtr  28952  sltval2  29384  ordtopcon  29872  ordtopt0  29875  wl-lem-moexsb  29985  filnetlem4  30167  seqpo  30208  fphpd  30718  pellexlem3  30735  qirropth  30812  expdioph  30933  rpnnen3  30942  iotasbc  31273  2reu1  32025  2reu3  32027  rlimdmafv  32096  fzoopth  32174  2ffzoeq  32175  usgra2pthspth  32185  islinindfis  32760  lincresunit3lem3  32785  bj-dfbi6  33851  bj-19.9htbi  33971  bj-ax16gb  34037  bj-equs5v  34044  bj-sb4bv  34050  lshpcmp  34415  lsatcmp  34430  lsatcmp2  34431  ltrneq2  35574  ltrneq  35575  tendospcanN  36452  dochlkr  36814  lcfl7N  36930  hgmap11  37334
  Copyright terms: Public domain W3C validator