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  501  ibar  502  pm5.71  934  cad0  1471  19.33b  1701  19.40b  1703  19.9t  1895  ax16gb  1947  equs5  2094  sb4b  2100  2eu1  2373  2eu1OLD  2374  2eu3  2376  ceqsalgALT  3132  csbprc  3820  undif4  3871  sneqbg  4186  opthpr  4194  elpwuni  4406  eusv2i  4634  reusv2lem3  4640  reusv3  4645  reuxfr2d  4660  ordssun  4966  suc11  4970  unizlim  4983  soltmin  5391  ssxpb  5426  xp11  5427  xpcan  5428  xpcan2  5429  iotanul  5549  imadif  5645  2elresin  5674  mpteqb  5946  f1fveq  6145  f1elima  6146  f1imass  6147  fliftf  6188  sorpssuni  6562  sorpssint  6563  iunpw  6587  ssonprc  6600  onint0  6604  oa00  7200  omcan  7210  omopth2  7225  oecan  7230  nnarcl  7257  iserd  7329  ecopover  7407  map0g  7451  fundmen  7582  fopwdom  7618  onfin  7701  fineqvlem  7727  f1finf1o  7739  isfiniteg  7772  inficl  7877  tc00  8170  cardnueq0  8336  cardsdomel  8346  wdomfil  8433  wdomnumr  8436  alephsucdom  8451  cardalephex  8462  dfac12lem2  8515  cfeq0  8627  fin23lem24  8693  fin1a2lem9  8779  carden  8917  axrepnd  8960  axacndlem4  8977  gchpwdom  9037  gchina  9066  r1tskina  9149  addcanpi  9266  mulcanpi  9267  elnpi  9355  addcan  9753  addcan2  9754  neg11  9861  negreb  9875  add20  10060  mulcand  10178  cru  10523  nn0lt10b  10921  uz11  11104  eqreznegel  11168  lbzbi  11171  rpnnen1  11214  xrmaxlt  11385  xrltmin  11386  xrmaxle  11387  xrlemin  11388  xneg11  11417  xsubge0  11456  xrub  11506  elioc2  11590  elico2  11591  elicc2  11592  fzopth  11724  2ffzeq  11798  flidz  11928  expeq0  12178  sq01  12270  fz1eqb  12408  hashen1  12422  hash1snb  12463  wrdnval  12559  eqwrd  12570  wrdl1s1  12611  ccatopth  12686  ccatopth2  12687  wrdlen2  12877  cj11  13077  sqrt0  13157  abs00  13204  recan  13251  rlimdm  13456  rpnnen2  14043  0dvds  14088  dvds1  14118  alzdvds  14120  gcdeq0  14243  algcvgblem  14290  prmexpb  14342  prmreclem3  14520  4sqlem11  14557  moni  15224  grprcan  16282  grplcan  16301  grpinv11  16306  galcan  16541  sylow2a  16838  subgdisjb  16910  drngmuleq0  17614  lspsncmp  17957  fidomndrng  18151  coe1tm  18509  xrsdsreclb  18660  znidomb  18773  lmisfree  19044  istps2OLD  19589  tgdom  19647  en1top  19653  cmpfi  20075  txcmpb  20311  hmeocnvb  20441  flimcls  20652  hauspwpwf1  20654  flftg  20663  ghmcnp  20779  metrest  21193  icoopnst  21605  iocopnst  21606  ishl2  21976  vitali  22188  mbfi1fseqlem4  22291  aannenlem1  22890  perfect  23704  usgra1v  24592  is2wlk  24769  usgra2wlkspth  24823  usg2wotspth  25086  usg2spot2nb  25267  extwwlkfab  25292  grporcan  25421  grpolcan  25433  ip2eqi  25970  hial2eq  26221  eigorthi  26954  stge1i  27355  stle0i  27356  mdbr3  27414  mdbr4  27415  atsseq  27464  mdsymlem7  27526  eqvincg  27572  reuxfr3d  27586  disjunsn  27664  fpwrelmapffslem  27786  xmulcand  27851  prsdm  28131  prsrn  28132  mthmpps  29206  untangtr  29327  sltval2  29656  ordtopcon  30132  ordtopt0  30135  wl-lem-moexsb  30257  filnetlem4  30439  seqpo  30480  fphpd  30989  pellexlem3  31006  qirropth  31083  expdioph  31204  rpnnen3  31213  iotasbc  31567  2reu1  32430  2reu3  32432  rlimdmafv  32501  fzoopth  32714  2ffzoeq  32715  usgra2pthspth  32723  0ringdif  32930  islinindfis  33304  lincresunit3lem3  33329  nn0enne  33390  blen1b  33463  bj-dfbi6  34557  bj-19.9htbi  34658  bj-ax16gb  34726  bj-equs5v  34733  bj-sb4bv  34739  lshpcmp  35110  lsatcmp  35125  lsatcmp2  35126  ltrneq2  36269  ltrneq  36270  tendospcanN  37147  dochlkr  37509  lcfl7N  37625  hgmap11  38029
  Copyright terms: Public domain W3C validator