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  523  ibar  524  pm5.71  997  cad0  1596  19.33b  1853  19.40b  1855  19.9t  2109  axc16gb  2174  19.9tOLD  2240  equs5  2379  sb4b  2386  2eu1  2582  2eu3  2584  ceqsalgALT  3262  eqvincg  3360  csbprcOLD  4014  undif4  4068  ssprsseq  4389  sneqbg  4406  preq1b  4409  opthpr  4415  elpwuni  4648  disjxiun  4681  eusv2i  4893  reusv2lem3  4901  reusv3  4906  reuxfr2d  4921  soltmin  5567  ssxpb  5603  xp11  5604  xpcan  5605  xpcan2  5606  ordssun  5865  suc11  5869  unizlim  5882  imadif  6011  2elresin  6040  mpteqb  6338  f1fveq  6559  f1elima  6560  f1imass  6561  fliftf  6605  sorpssuni  6988  sorpssint  6989  iunpw  7020  ssonprc  7034  onint0  7038  oa00  7684  omcan  7694  omopth2  7709  oecan  7714  nnarcl  7741  iserd  7813  map0g  7939  fundmen  8071  fopwdom  8109  onfin  8192  fineqvlem  8215  f1finf1o  8228  isfiniteg  8261  inficl  8372  tc00  8662  cardnueq0  8828  cardsdomel  8838  wdomfil  8922  wdomnumr  8925  alephsucdom  8940  cardalephex  8951  dfac12lem2  9004  cfeq0  9116  fin23lem24  9182  fin1a2lem9  9268  carden  9411  axrepnd  9454  axacndlem4  9470  gchpwdom  9530  gchina  9559  r1tskina  9642  addcanpi  9759  mulcanpi  9760  elnpi  9848  addcan  10258  addcan2  10259  neg11  10370  negreb  10384  add20  10578  mulcand  10698  cru  11050  nn0lt10b  11477  uz11  11748  eqreznegel  11812  lbzbi  11814  rpnnen1lem6  11857  rpnnen1OLD  11863  xrmaxlt  12050  xrltmin  12051  xrmaxle  12052  xrlemin  12053  xneg11  12084  xnn0xadd0  12115  xsubge0  12129  xrub  12180  elioc2  12274  elico2  12275  elicc2  12276  fzopth  12416  2ffzeq  12499  flidz  12651  addmodlteq  12785  expeq0  12930  sq01  13026  fz1eqb  13183  hashen1  13198  hash1snb  13245  hashle2pr  13297  wrdnval  13367  eqwrd  13379  ccatalpha  13411  wrdl1s1  13431  ccats1alpha  13436  ccatopth  13516  ccatopth2  13517  wrdlen2  13734  cj11  13946  sqrt0  14026  abs00  14073  recan  14120  rlimdm  14326  rpnnen2lem12  14998  0dvds  15049  dvds1  15088  alzdvds  15089  nn0enne  15141  nn0oddm1d2  15148  nnoddm1d2  15149  gcdeq0  15285  algcvgblem  15337  prmexpb  15477  prmreclem3  15669  4sqlem11  15706  moni  16443  grprcan  17502  grplcan  17524  grpinv11  17531  galcan  17783  sylow2a  18080  subgdisjb  18152  drngmuleq0  18818  lspsncmp  19164  fidomndrng  19355  coe1tm  19691  xrsdsreclb  19841  znidomb  19958  lmisfree  20229  tgdom  20830  en1top  20836  cmpfi  21259  txcmpb  21495  hmeocnvb  21625  flimcls  21836  hauspwpwf1  21838  flftg  21847  ghmcnp  21965  metrest  22376  icoopnst  22785  iocopnst  22786  ishl2  23212  vitali  23427  mbfi1fseqlem4  23530  aannenlem1  24128  perfect  25001  2lgsoddprmlem3  25184  umgrislfupgrlem  26062  usgrausgrb  26109  cplgruvtxbOLD  26367  upgriswlk  26593  uhgrwkspth  26707  usgr2wlkspth  26711  usgr2trlspth  26713  usgr2pthspth  26714  extwwlkfab  27342  grporcan  27500  grpolcan  27512  ip2eqi  27840  hial2eq  28091  eigorthi  28824  stge1i  29225  stle0i  29226  mdbr3  29284  mdbr4  29285  atsseq  29334  mdsymlem7  29396  reuxfr3d  29456  disjunsn  29533  fpwrelmapffslem  29635  xmulcand  29757  prsdm  30088  prsrn  30089  mthmpps  31605  untangtr  31717  funeldmb  31787  sltval2  31934  filnetlem4  32501  ordtopconn  32563  ordtopt0  32566  bj-dfbi6  32685  bj-19.9htbi  32819  icorempt2  33329  wl-lem-moexsb  33480  seqpo  33673  lshpcmp  34593  lsatcmp  34608  lsatcmp2  34609  ltrneq2  35752  ltrneq  35753  tendospcanN  36629  dochlkr  36991  lcfl7N  37107  hgmap11  37511  fphpd  37697  pellexlem3  37712  qirropth  37790  expdioph  37907  rpnnen3  37916  iotasbc  38937  2reu1  41507  2reu3  41509  rlimdmafv  41578  funop1  41625  fzoopth  41662  2ffzoeq  41663  evenprm2  41948  perfectALTV  41957  nnsum3primesle9  42007  upgrwlkupwlkb  42047  0ringdif  42195  islinindfis  42563  lincresunit3lem3  42588  blen1b  42707
  Copyright terms: Public domain W3C validator