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  525  ibar  526  pm5.71  1015  cad0  1705  19.33b  1962  19.40b  1964  19.9t  2218  axc16gb  2283  19.9tOLD  2349  equs5  2488  sb4b  2495  2eu1  2691  2eu3  2693  ceqsalgALT  3371  eqvincg  3468  csbprcOLD  4124  disjeq0  4166  undif4  4179  ssprsseq  4502  sneqbg  4519  preq1b  4522  opthpr  4528  preq12nebg  4543  opthprneg  4545  elpwuni  4768  disjxiun  4801  eusv2i  5012  reusv2lem3  5020  reusv3  5025  reuxfr2d  5040  soltmin  5690  ssxpb  5726  xp11  5727  xpcan  5728  xpcan2  5729  ordssun  5988  suc11  5992  unizlim  6005  imadif  6134  2elresin  6163  mpteqb  6462  f1fveq  6683  f1elima  6684  f1imass  6685  fliftf  6729  sorpssuni  7112  sorpssint  7113  iunpw  7144  ssonprc  7158  onint0  7162  oa00  7810  omcan  7820  omopth2  7835  oecan  7840  nnarcl  7867  iserd  7939  map0g  8065  fundmen  8197  fopwdom  8235  onfin  8318  fineqvlem  8341  f1finf1o  8354  isfiniteg  8387  inficl  8498  tc00  8799  cardnueq0  9000  cardsdomel  9010  wdomfil  9094  wdomnumr  9097  alephsucdom  9112  cardalephex  9123  dfac12lem2  9178  cfeq0  9290  fin23lem24  9356  fin1a2lem9  9442  carden  9585  axrepnd  9628  axacndlem4  9644  gchpwdom  9704  gchina  9733  r1tskina  9816  addcanpi  9933  mulcanpi  9934  elnpi  10022  addcan  10432  addcan2  10433  neg11  10544  negreb  10558  add20  10752  mulcand  10872  cru  11224  nn0lt10b  11651  uz11  11922  eqreznegel  11987  lbzbi  11989  rpnnen1lem6  12032  rpnnen1OLD  12038  xrmaxlt  12225  xrltmin  12226  xrmaxle  12227  xrlemin  12228  xneg11  12259  xnn0xadd0  12290  xsubge0  12304  xrub  12355  elioc2  12449  elico2  12450  elicc2  12451  fzopth  12591  2ffzeq  12674  flidz  12825  addmodlteq  12959  expeq0  13104  sq01  13200  fz1eqb  13357  hashen1  13372  hash1snb  13419  hashle2pr  13471  wrdnval  13541  eqwrd  13553  ccatalpha  13585  wrdl1s1  13605  ccats1alpha  13610  ccatopth  13690  ccatopth2  13691  wrdlen2  13909  cj11  14121  sqrt0  14201  abs00  14248  recan  14295  rlimdm  14501  rpnnen2lem12  15173  0dvds  15224  dvds1  15263  alzdvds  15264  nn0enne  15316  nn0oddm1d2  15323  nnoddm1d2  15324  gcdeq0  15460  algcvgblem  15512  prmexpb  15652  prmreclem3  15844  4sqlem11  15881  moni  16617  grprcan  17676  grplcan  17698  grpinv11  17705  galcan  17957  sylow2a  18254  subgdisjb  18326  drngmuleq0  18992  lspsncmp  19338  fidomndrng  19529  coe1tm  19865  xrsdsreclb  20015  znidomb  20132  lmisfree  20403  tgdom  21004  en1top  21010  cmpfi  21433  txcmpb  21669  hmeocnvb  21799  flimcls  22010  hauspwpwf1  22012  flftg  22021  ghmcnp  22139  metrest  22550  icoopnst  22959  iocopnst  22960  ishl2  23386  vitali  23601  mbfi1fseqlem4  23704  aannenlem1  24302  perfect  25176  2lgsoddprmlem3  25359  umgrislfupgrlem  26237  usgrausgrb  26284  cplgruvtxbOLD  26542  upgriswlk  26768  uhgrwkspth  26882  usgr2wlkspth  26886  usgr2trlspth  26888  usgr2pthspth  26889  extwwlkfab  27532  grporcan  27702  grpolcan  27714  ip2eqi  28042  hial2eq  28293  eigorthi  29026  stge1i  29427  stle0i  29428  mdbr3  29486  mdbr4  29487  atsseq  29536  mdsymlem7  29598  reuxfr3d  29658  disjunsn  29735  fpwrelmapffslem  29837  xmulcand  29959  prsdm  30290  prsrn  30291  mthmpps  31807  untangtr  31919  funeldmb  31989  sltval2  32136  filnetlem4  32703  ordtopconn  32765  ordtopt0  32768  bj-dfbi6  32888  bj-19.9htbi  33022  icorempt2  33528  wl-lem-moexsb  33681  seqpo  33874  lshpcmp  34796  lsatcmp  34811  lsatcmp2  34812  ltrneq2  35955  ltrneq  35956  tendospcanN  36832  dochlkr  37194  lcfl7N  37310  hgmap11  37714  fphpd  37900  pellexlem3  37915  qirropth  37993  expdioph  38110  rpnnen3  38119  iotasbc  39140  2reu1  41710  2reu3  41712  rlimdmafv  41781  funop1  41828  fzoopth  41865  2ffzoeq  41866  evenprm2  42151  perfectALTV  42160  nnsum3primesle9  42210  upgrwlkupwlkb  42250  0ringdif  42398  islinindfis  42766  lincresunit3lem3  42791  blen1b  42910
  Copyright terms: Public domain W3C validator