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

Theorem impbid1 216
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 203 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197
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 198
This theorem is referenced by:  impbid2  217  iba  519  ibar  520  pm5.71  1043  cad0  1711  19.33b  1975  19.40b  1977  19.9t  2239  axc16gb  2315  19.9tOLD  2380  equs5  2511  sb4b  2519  2eu1  2724  2eu3  2726  ceqsalgALT  3432  eqvincg  3530  disjeq0  4227  undif4  4238  ssprsseq  4553  sneqbg  4569  preq1b  4572  opthpr  4578  preq12nebg  4592  opthprneg  4594  elpwuni  4815  disjxiun  4848  eusv2i  5070  reusv2lem3  5076  reusv3  5081  reuxfr2d  5095  soltmin  5750  ssxpb  5786  xp11  5787  xpcan  5788  xpcan2  5789  ordssun  6043  suc11  6047  unizlim  6060  imadif  6187  2elresin  6216  mpteqb  6523  f1fveq  6746  f1elima  6747  f1imass  6748  fliftf  6792  sorpssuni  7179  sorpssint  7180  iunpw  7211  ssonprc  7225  onint0  7229  oa00  7879  omcan  7889  omopth2  7904  oecan  7909  nnarcl  7936  iserd  8008  map0g  8136  fundmen  8269  fopwdom  8310  onfin  8393  fineqvlem  8416  f1finf1o  8429  isfiniteg  8462  inficl  8573  tc00  8874  cardnueq0  9076  cardsdomel  9086  wdomfil  9170  wdomnumr  9173  alephsucdom  9188  cardalephex  9199  dfac12lem2  9254  cfeq0  9366  fin23lem24  9432  fin1a2lem9  9518  carden  9661  axrepnd  9704  axacndlem4  9720  gchpwdom  9780  gchina  9809  r1tskina  9892  addcanpi  10009  mulcanpi  10010  elnpi  10098  addcan  10508  addcan2  10509  neg11  10620  negreb  10634  add20  10828  mulcand  10948  cru  11300  nn0lt10b  11708  uz11  11930  eqreznegel  11996  lbzbi  11998  rpnnen1lem6  12041  xrmaxlt  12233  xrltmin  12234  xrmaxle  12235  xrlemin  12236  xneg11  12267  xnn0xadd0  12298  xsubge0  12312  xrub  12363  elioc2  12457  elico2  12458  elicc2  12459  fzopth  12604  2ffzeq  12687  flidz  12838  addmodlteq  12972  expeq0  13116  sq01  13212  fz1eqb  13366  hashen1  13381  hash1snb  13427  hashle2pr  13479  wrdnval  13549  eqwrd  13561  ccatalpha  13593  wrdl1s1  13612  ccats1alpha  13617  ccatopth  13697  ccatopth2  13698  wrdlen2  13916  cj11  14128  sqrt0  14208  abs00  14255  recan  14302  rlimdm  14508  rpnnen2lem12  15177  0dvds  15228  dvds1  15267  alzdvds  15268  nn0enne  15317  nn0oddm1d2  15324  nnoddm1d2  15325  gcdeq0  15460  algcvgblem  15512  prmexpb  15650  prmreclem3  15842  4sqlem11  15879  moni  16603  grprcan  17663  grplcan  17685  grpinv11  17692  galcan  17941  sylow2a  18238  subgdisjb  18310  drngmuleq0  18977  lspsncmp  19326  fidomndrng  19519  coe1tm  19854  xrsdsreclb  20004  znidomb  20120  lmisfree  20395  tgdom  21000  en1top  21006  cmpfi  21429  txcmpb  21665  hmeocnvb  21795  flimcls  22006  hauspwpwf1  22008  flftg  22017  ghmcnp  22135  metrest  22546  icoopnst  22955  iocopnst  22956  ishl2  23383  vitali  23600  mbfi1fseqlem4  23705  aannenlem1  24303  perfect  25176  2lgsoddprmlem3  25359  umgrislfupgrlem  26237  usgrausgrb  26285  cplgruvtxbOLD  26545  upgriswlk  26771  uhgrwkspth  26885  usgr2wlkspth  26889  usgr2trlspth  26891  usgr2pthspth  26892  extwwlkfab  27537  grporcan  27707  grpolcan  27719  ip2eqi  28046  hial2eq  28297  eigorthi  29030  stge1i  29431  stle0i  29432  mdbr3  29490  mdbr4  29491  atsseq  29540  mdsymlem7  29602  reuxfr3d  29661  disjunsn  29738  fpwrelmapffslem  29840  xmulcand  29960  prsdm  30291  prsrn  30292  mthmpps  31807  untangtr  31918  funeldmb  31988  sltval2  32135  filnetlem4  32702  ordtopconn  32760  ordtopt0  32763  bj-dfbi6  32879  bj-19.9htbi  33014  icorempt2  33517  wl-lem-moexsb  33666  seqpo  33856  lshpcmp  34770  lsatcmp  34785  lsatcmp2  34786  ltrneq2  35930  ltrneq  35931  tendospcanN  36805  dochlkr  37167  lcfl7N  37283  hgmap11  37684  fphpd  37883  pellexlem3  37898  qirropth  37975  expdioph  38092  rpnnen3  38101  iotasbc  39120  2reu1  41699  2reu3  41701  rlimdmafv  41767  afv2orxorb  41818  rlimdmafv2  41848  funop1  41874  fzoopth  41913  2ffzoeq  41914  evenprm2  42199  perfectALTV  42208  nnsum3primesle9  42258  upgrwlkupwlkb  42291  0ringdif  42439  islinindfis  42807  lincresunit3lem3  42832  blen1b  42951
  Copyright terms: Public domain W3C validator