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

Theorem impbid1 228
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 215 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209
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 210
This theorem is referenced by:  impbid2  229  iba  531  pm5.61  998  pm5.71  1025  cad0  1619  19.33b  1886  19.40b  1889  19.9t  2202  axc16gb  2260  equs5  2472  2eu1  2712  2eu1v  2713  2eu3  2715  ceqsalgALT  3477  eqvincg  3589  reuxfrd  3687  2reu1  3826  disjeq0  4363  undif4  4374  ssprsseq  4718  sneqbg  4734  preq1b  4737  opthpr  4742  preq12nebg  4753  opthprneg  4755  elpwuni  4990  disjxiun  5027  eusv2i  5260  reusv2lem3  5266  reusv3  5271  soltmin  5963  ssxpb  5998  xp11  5999  xpcan  6000  xpcan2  6001  ordssun  6258  suc11  6262  unizlim  6275  imadif  6408  2elresin  6440  mpteqb  6764  f1fveq  6998  f1elima  6999  f1imass  7000  fliftf  7047  sorpssuni  7438  sorpssint  7439  iunpw  7473  ssonprc  7487  onint0  7491  oa00  8168  omcan  8178  omopth2  8193  oecan  8198  nnarcl  8225  iserd  8298  map0g  8431  fundmen  8566  fopwdom  8608  onfin  8694  fineqvlem  8716  f1finf1o  8729  isfiniteg  8762  inficl  8873  tc00  9174  cardnueq0  9377  cardsdomel  9387  wdomfil  9472  wdomnumr  9475  alephsucdom  9490  cardalephex  9501  dfac12lem2  9555  cfeq0  9667  fin23lem24  9733  fin1a2lem9  9819  carden  9962  axrepnd  10005  axacndlem4  10021  gchpwdom  10081  gchina  10110  r1tskina  10193  addcanpi  10310  mulcanpi  10311  elnpi  10399  addcan  10813  addcan2  10814  neg11  10926  negreb  10940  add20  11141  mulcand  11262  cru  11617  nn0lt10b  12032  uz11  12255  eqreznegel  12322  lbzbi  12324  rpnnen1lem6  12369  xrmaxlt  12562  xrltmin  12563  xrmaxle  12564  xrlemin  12565  xneg11  12596  xnn0xadd0  12628  xsubge0  12642  xrub  12693  elioc2  12788  elico2  12789  elicc2  12790  fzopth  12939  2ffzeq  13023  flidz  13175  addmodlteq  13309  expeq0  13455  sq01  13582  fz1eqb  13711  hashen1  13727  hash1snb  13776  hashle2pr  13831  wrdnval  13888  eqwrd  13900  ccatalpha  13938  wrdl1s1  13959  ccats1alpha  13964  ccatopth  14069  ccatopth2  14070  wrdlen2  14297  cj11  14513  sqrt0  14593  abs00  14641  recan  14688  cnsqrt00  14744  rlimdm  14900  rpnnen2lem12  15570  0dvds  15622  dvds1  15661  alzdvds  15662  nn0enne  15718  nn0oddm1d2  15726  nnoddm1d2  15727  gcdeq0  15855  algcvgblem  15911  2mulprm  16027  prmexpb  16052  prmreclem3  16244  4sqlem11  16281  moni  16998  grprcan  18129  grplcan  18153  grpinv11  18160  galcan  18426  sylow2a  18736  subgdisjb  18811  drngmuleq0  19518  lspsncmp  19881  fidomndrng  20073  xrsdsreclb  20138  znidomb  20253  lmisfree  20531  coe1tm  20902  tgdom  21583  en1top  21589  cmpfi  22013  txcmpb  22249  hmeocnvb  22379  flimcls  22590  hauspwpwf1  22592  flftg  22601  ghmcnp  22720  metrest  23131  icoopnst  23544  iocopnst  23545  ishl2  23974  vitali  24217  mbfi1fseqlem4  24322  aannenlem1  24924  perfect  25815  2lgsoddprmlem3  25998  2sq2  26017  umgrislfupgrlem  26915  usgrausgrb  26962  upgriswlk  27430  uhgrwkspth  27544  usgr2wlkspth  27548  usgr2trlspth  27550  usgr2pthspth  27551  extwwlkfab  28137  grporcan  28301  grpolcan  28313  ip2eqi  28639  hial2eq  28889  eigorthi  29620  stge1i  30021  stle0i  30022  mdbr3  30080  mdbr4  30081  atsseq  30130  mdsymlem7  30192  reuxfrdf  30262  disjunsn  30357  fpwrelmapffslem  30494  xmulcand  30623  prsdm  31267  prsrn  31268  lfuhgr  32474  lfuhgr2  32475  mthmpps  32939  untangtr  33050  funeldmb  33116  sltval2  33273  filnetlem4  33839  ordtopconn  33897  ordtopt0  33900  bj-dfbi6  34018  bj-19.9htbi  34147  bj-elid6  34582  icorempo  34765  inunissunidif  34789  fvineqsneu  34825  wl-lem-moexsb  34966  seqpo  35182  lshpcmp  36281  lsatcmp  36296  lsatcmp2  36297  ltrneq2  37441  ltrneq  37442  tendospcanN  38316  dochlkr  38678  lcfl7N  38794  hgmap11  39195  ccatcan2d  39417  remulcan2d  39459  resubcan2  39521  readdcan2  39545  sn-addcand  39551  sn-addcan2d  39553  remulcand  39570  itrere  39586  retire  39587  cnreeu  39588  fphpd  39752  pellexlem3  39767  qirropth  39844  expdioph  39959  rpnnen3  39968  iotasbc  41118  2reu3  43661  rlimdmafv  43728  afv2orxorb  43779  rlimdmafv2  43809  funop1  43834  fzoopth  43879  2ffzoeq  43880  prprelprb  44029  poprelb  44036  evenprm2  44227  perfectALTV  44236  nnsum3primesle9  44307  upgrwlkupwlkb  44364  0ringdif  44489  islinindfis  44853  lincresunit3lem3  44878  blen1b  44997  line2ylem  45160  line2y  45164
  Copyright terms: Public domain W3C validator