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

Theorem impbid1 215
Description: Infer an equivalence from two implications. (Contributed by NM, 6-Mar-2007.)
Hypotheses
Ref Expression
impbid1.1 (𝜑 → (𝜓𝜒))
impbid1.2 (𝜒𝜓)
Assertion
Ref Expression
impbid1 (𝜑 → (𝜓𝜒))

Proof of Theorem impbid1
StepHypRef Expression
1 impbid1.1 . 2 (𝜑 → (𝜓𝜒))
2 impbid1.2 . . 3 (𝜒𝜓)
32a1i 11 . 2 (𝜑 → (𝜒𝜓))
41, 3impbid 202 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
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 197
This theorem is referenced by:  impbid2  216  iba  524  ibar  525  pm5.71  976  cad0  1553  19.33b  1810  19.40b  1812  19.9t  2069  axc16gb  2132  19.9tOLD  2203  equs5  2350  sb4b  2357  2eu1  2552  2eu3  2554  ceqsalgALT  3221  csbprcOLD  3959  undif4  4013  ssprsseq  4332  sneqbg  4349  preq1b  4352  opthpr  4359  elpwuni  4589  disjxiun  4619  eusv2i  4833  reusv2lem3  4841  reusv3  4846  reuxfr2d  4861  soltmin  5501  ssxpb  5537  xp11  5538  xpcan  5539  xpcan2  5540  ordssun  5796  suc11  5800  unizlim  5813  imadif  5941  2elresin  5970  mpteqb  6265  f1fveq  6484  f1elima  6485  f1imass  6486  fliftf  6530  sorpssuni  6911  sorpssint  6912  iunpw  6940  ssonprc  6954  onint0  6958  oa00  7599  omcan  7609  omopth2  7624  oecan  7629  nnarcl  7656  iserd  7728  ecopoverOLD  7812  map0g  7857  fundmen  7990  fopwdom  8028  onfin  8111  fineqvlem  8134  f1finf1o  8147  isfiniteg  8180  inficl  8291  tc00  8584  cardnueq0  8750  cardsdomel  8760  wdomfil  8844  wdomnumr  8847  alephsucdom  8862  cardalephex  8873  dfac12lem2  8926  cfeq0  9038  fin23lem24  9104  fin1a2lem9  9190  carden  9333  axrepnd  9376  axacndlem4  9392  gchpwdom  9452  gchina  9481  r1tskina  9564  addcanpi  9681  mulcanpi  9682  elnpi  9770  addcan  10180  addcan2  10181  neg11  10292  negreb  10306  add20  10500  mulcand  10620  cru  10972  nn0lt10b  11399  uz11  11670  eqreznegel  11734  lbzbi  11736  rpnnen1lem6  11779  rpnnen1OLD  11785  xrmaxlt  11971  xrltmin  11972  xrmaxle  11973  xrlemin  11974  xneg11  12005  xnn0xadd0  12036  xsubge0  12050  xrub  12101  elioc2  12194  elico2  12195  elicc2  12196  fzopth  12336  2ffzeq  12417  flidz  12567  addmodlteq  12701  expeq0  12846  sq01  12942  fz1eqb  13101  hashen1  13116  hash1snb  13163  hashle2pr  13213  wrdnval  13290  eqwrd  13301  ccatalpha  13330  wrdl1s1  13349  ccatopth  13424  ccatopth2  13425  wrdlen2  13638  cj11  13852  sqrt0  13932  abs00  13979  recan  14026  rlimdm  14232  rpnnen2lem12  14898  0dvds  14945  dvds1  14984  alzdvds  14985  nn0enne  15037  nn0oddm1d2  15044  nnoddm1d2  15045  gcdeq0  15181  algcvgblem  15233  prmexpb  15373  prmreclem3  15565  4sqlem11  15602  moni  16336  grprcan  17395  grplcan  17417  grpinv11  17424  galcan  17677  sylow2a  17974  subgdisjb  18046  drngmuleq0  18710  lspsncmp  19056  fidomndrng  19247  coe1tm  19583  xrsdsreclb  19733  znidomb  19850  lmisfree  20121  tgdom  20722  en1top  20728  cmpfi  21151  txcmpb  21387  hmeocnvb  21517  flimcls  21729  hauspwpwf1  21731  flftg  21740  ghmcnp  21858  metrest  22269  icoopnst  22678  iocopnst  22679  ishl2  23106  vitali  23322  mbfi1fseqlem4  23425  aannenlem1  24021  perfect  24890  2lgsoddprmlem3  25073  umgrislfupgrlem  25946  usgrausgrb  25991  cplgruvtxb  26232  upgriswlk  26440  uhgrwkspth  26554  usgr2wlkspth  26558  usgr2trlspth  26560  usgr2pthspth  26561  extwwlkfab  27112  grporcan  27260  grpolcan  27272  ip2eqi  27600  hial2eq  27851  eigorthi  28584  stge1i  28985  stle0i  28986  mdbr3  29044  mdbr4  29045  atsseq  29094  mdsymlem7  29156  eqvincg  29202  reuxfr3d  29218  disjunsn  29293  fpwrelmapffslem  29391  xmulcand  29456  prsdm  29784  prsrn  29785  mthmpps  31240  untangtr  31352  sltval2  31563  filnetlem4  32071  ordtopconn  32133  ordtopt0  32136  bj-dfbi6  32255  bj-19.9htbi  32389  icorempt2  32870  wl-lem-moexsb  33021  seqpo  33214  lshpcmp  33794  lsatcmp  33809  lsatcmp2  33810  ltrneq2  34953  ltrneq  34954  tendospcanN  35831  dochlkr  36193  lcfl7N  36309  hgmap11  36713  fphpd  36899  pellexlem3  36914  qirropth  36992  expdioph  37109  rpnnen3  37118  iotasbc  38141  2reu1  40520  2reu3  40522  rlimdmafv  40591  funop1  40629  fzoopth  40664  2ffzoeq  40665  evenprm2  40952  perfectALTV  40957  nnsum3primesle9  41001  upgrwlkupwlkb  41040  0ringdif  41188  islinindfis  41556  lincresunit3lem3  41581  blen1b  41704
  Copyright terms: Public domain W3C validator