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  1452  19.33b  1673  19.9t  1838  ax16gb  1889  equs5  2065  sb4b  2071  euor2OLD  2335  eupickbiOLD  2369  2eu1  2386  2eu1OLD  2387  2eu3  2389  ceqsalgALT  3139  csbprc  3821  undif4  3883  sneqbg  4197  opthpr  4204  elpwuni  4413  eusv2i  4644  reusv2lem3  4650  reusv3  4655  reuxfr2d  4670  ordssun  4977  suc11  4981  unizlim  4994  soltmin  5406  ssxpb  5441  xp11  5442  xpcan  5443  xpcan2  5444  iotanul  5566  imadif  5663  2elresin  5692  mpteqb  5964  f1fveq  6158  f1elima  6159  f1imass  6160  fliftf  6201  sorpssuni  6573  sorpssint  6574  iunpw  6598  ssonprc  6611  onint0  6615  oa00  7208  omcan  7218  omopth2  7233  oecan  7238  nnarcl  7265  iserd  7337  ecopover  7415  map0g  7458  fundmen  7589  fopwdom  7625  onfin  7708  fineqvlem  7734  f1finf1o  7746  isfiniteg  7780  inficl  7885  tc00  8179  cardnueq0  8345  cardsdomel  8355  wdomfil  8442  wdomnumr  8445  alephsucdom  8460  cardalephex  8471  dfac12lem2  8524  cfeq0  8636  fin23lem24  8702  fin1a2lem9  8788  carden  8926  axrepnd  8969  axacndlem4  8988  gchpwdom  9048  gchina  9077  r1tskina  9160  addcanpi  9277  mulcanpi  9278  elnpi  9366  addcan  9763  addcan2  9764  neg11  9870  negreb  9884  add20  10064  mulcand  10182  cru  10528  uz11  11104  eqreznegel  11167  lbzbi  11170  rpnnen1  11213  xrmaxlt  11382  xrltmin  11383  xrmaxle  11384  xrlemin  11385  xneg11  11414  xsubge0  11453  xrub  11503  elioc2  11587  elico2  11588  elicc2  11589  fzopth  11720  2ffzeq  11791  flidz  11915  expeq0  12164  sq01  12256  fz1eqb  12394  hashen1  12407  hash1snb  12444  wrdnval  12537  eqwrd  12547  wrdl1s1  12585  ccatopth  12658  ccatopth2  12659  wrdlen2  12849  cj11  12958  sqrt0  13038  abs00  13085  recan  13132  rlimdm  13337  rpnnen2  13820  0dvds  13865  dvds1  13893  alzdvds  13895  gcdeq0  14018  algcvgblem  14065  prmexpb  14117  prmreclem3  14295  4sqlem11  14332  moni  14992  grprcan  15893  grplcan  15912  grpinv11  15917  galcan  16147  sylow2a  16445  subgdisjb  16517  drngmuleq0  17219  lspsncmp  17562  fidomndrng  17755  coe1tm  18113  xrsdsreclb  18261  znidomb  18395  lmisfree  18672  istps2OLD  19217  tgdom  19274  en1top  19280  cmpfi  19702  txcmpb  19908  hmeocnvb  20038  flimcls  20249  hauspwpwf1  20251  flftg  20260  ghmcnp  20376  metrest  20790  icoopnst  21202  iocopnst  21203  ishl2  21573  vitali  21785  mbfi1fseqlem4  21888  aannenlem1  22486  perfect  23262  usgra1v  24094  is2wlk  24271  usgra2wlkspth  24325  usg2wotspth  24588  usg2spot2nb  24770  extwwlkfab  24795  grporcan  24927  grpolcan  24939  ip2eqi  25476  hial2eq  25727  eigorthi  26460  stge1i  26861  stle0i  26862  mdbr3  26920  mdbr4  26921  atsseq  26970  mdsymlem7  27032  eqvincg  27078  reuxfr3d  27092  xmulcand  27313  untangtr  28589  sltval2  29021  ordtopcon  29509  ordtopt0  29512  wl-sb6nae  29611  wl-lem-moexsb  29622  filnetlem4  29830  seqpo  29871  fphpd  30382  pellexlem3  30399  qirropth  30476  expdioph  30597  rpnnen3  30606  iotasbc  30932  2reu1  31686  2reu3  31688  rlimdmafv  31757  fzoopth  31835  2ffzoeq  31836  usgra2pthspth  31846  islinindfis  32149  lincresunit3lem3  32174  bj-dfbi6  33241  bj-19.40b  33326  bj-19.9htbi  33357  bj-ax16gb  33424  bj-equs5v  33431  bj-sb4bv  33437  lshpcmp  33803  lsatcmp  33818  lsatcmp2  33819  ltrneq2  34962  ltrneq  34963  tendospcanN  35838  dochlkr  36200  lcfl7N  36316  hgmap11  36720
  Copyright terms: Public domain W3C validator