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

Theorem impbid1 208
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 195 1  |-  ( ph  ->  ( ps  <->  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189
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 190
This theorem is referenced by:  impbid2  209  iba  510  ibar  511  pm5.71  952  cad0  1530  19.33b  1758  19.40b  1760  19.40bOLD  1761  19.9t  1979  19.9tOLD  1982  axc16gb  2035  equs5  2192  sb4b  2198  2eu1  2392  2eu3  2394  ceqsalgALT  3084  csbprc  3781  undif4  3832  sneqbg  4154  preq1b  4158  opthpr  4165  elpwuni  4382  eusv2i  4613  reusv2lem3  4619  reusv3  4624  reuxfr2d  4636  soltmin  5254  ssxpb  5289  xp11  5290  xpcan  5291  xpcan2  5292  ordssun  5540  suc11  5544  unizlim  5557  iotanul  5579  imadif  5679  2elresin  5708  mpteqb  5986  f1fveq  6187  f1elima  6188  f1imass  6189  fliftf  6232  sorpssuni  6606  sorpssint  6607  iunpw  6631  ssonprc  6645  onint0  6649  oa00  7285  omcan  7295  omopth2  7310  oecan  7315  nnarcl  7342  iserd  7414  ecopover  7492  map0g  7536  fundmen  7668  fopwdom  7705  onfin  7788  fineqvlem  7811  f1finf1o  7823  isfiniteg  7856  inficl  7964  tc00  8257  cardnueq0  8423  cardsdomel  8433  wdomfil  8517  wdomnumr  8520  alephsucdom  8535  cardalephex  8546  dfac12lem2  8599  cfeq0  8711  fin23lem24  8777  fin1a2lem9  8863  carden  9001  axrepnd  9044  axacndlem4  9060  gchpwdom  9120  gchina  9149  r1tskina  9232  addcanpi  9349  mulcanpi  9350  elnpi  9438  addcan  9842  addcan2  9843  neg11  9950  negreb  9964  add20  10153  mulcand  10272  cru  10628  nn0lt10b  11026  uz11  11209  eqreznegel  11277  lbzbi  11280  rpnnen1  11323  xrmaxlt  11504  xrltmin  11505  xrmaxle  11506  xrlemin  11507  xneg11  11536  xsubge0  11575  xrub  11625  elioc2  11725  elico2  11726  elicc2  11727  fzopth  11863  2ffzeq  11940  flidz  12077  expeq0  12333  sq01  12425  fz1eqb  12567  hashen1  12581  hash1snb  12625  wrdnval  12732  eqwrd  12743  wrdl1s1  12787  ccatopth  12862  ccatopth2  12863  wrdlen2  13068  cj11  13273  sqrt0  13353  abs00  13400  recan  13447  rlimdm  13663  rpnnen2  14326  0dvds  14371  dvds1  14401  alzdvds  14403  gcdeq0  14533  algcvgblem  14584  prmexpb  14718  prmreclem3  14910  4sqlem11  14947  moni  15689  grprcan  16747  grplcan  16766  grpinv11  16771  galcan  17006  sylow2a  17319  subgdisjb  17391  drngmuleq0  18046  lspsncmp  18387  fidomndrng  18579  coe1tm  18914  xrsdsreclb  19063  znidomb  19180  lmisfree  19448  tgdom  20042  en1top  20048  cmpfi  20471  txcmpb  20707  hmeocnvb  20837  flimcls  21048  hauspwpwf1  21050  flftg  21059  ghmcnp  21177  metrest  21587  icoopnst  22015  iocopnst  22016  ishl2  22385  vitali  22619  mbfi1fseqlem4  22724  aannenlem1  23332  perfect  24207  usgra1v  25165  is2wlk  25343  usgra2wlkspth  25397  usg2wotspth  25660  usg2spot2nb  25841  extwwlkfab  25866  grporcan  25997  grpolcan  26009  ip2eqi  26546  hial2eq  26807  eigorthi  27538  stge1i  27939  stle0i  27940  mdbr3  27998  mdbr4  27999  atsseq  28048  mdsymlem7  28110  eqvincg  28156  reuxfr3d  28173  disjunsn  28252  fpwrelmapffslem  28365  xmulcand  28438  prsdm  28768  prsrn  28769  mthmpps  30268  untangtr  30389  sltval2  30591  filnetlem4  31085  ordtopcon  31147  ordtopt0  31150  bj-dfbi6  31195  bj-19.9htbi  31341  bj-axc16gb  31401  bj-equs5v  31408  bj-sb4bv  31414  icorempt2  31798  wl-lem-moexsb  31941  seqpo  32120  lshpcmp  32598  lsatcmp  32613  lsatcmp2  32614  ltrneq2  33757  ltrneq  33758  tendospcanN  34635  dochlkr  34997  lcfl7N  35113  hgmap11  35517  fphpd  35703  pellexlem3  35719  qirropth  35800  expdioph  35922  rpnnen3  35931  iotasbc  36813  2reu1  38644  2reu3  38646  rlimdmafv  38716  evenprm2  38879  perfectALTV  38882  nnsum3primesle9  38926  ssprsseq  39041  funop1  39061  fzoopth  39104  2ffzoeq  39105  xnn0xadd0  39133  usgrausgrb  39303  cplgruvtxb  39532  upgr1wlkwlkb  39700  umgrislfupgrlem  39717  uhgr1wlkspth  39786  usgr2wlkspth  39790  usgra2pthspth  39937  0ringdif  40142  islinindfis  40514  lincresunit3lem3  40539  nn0enne  40598  blen1b  40671
  Copyright terms: Public domain W3C validator