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

Theorem impbida 794
Description: Deduce an equivalence from two implications. (Contributed by NM, 17-Feb-2007.)
Hypotheses
Ref Expression
impbida.1 ((𝜑𝜓) → 𝜒)
impbida.2 ((𝜑𝜒) → 𝜓)
Assertion
Ref Expression
impbida (𝜑 → (𝜓𝜒))

Proof of Theorem impbida
StepHypRef Expression
1 impbida.1 . . 3 ((𝜑𝜓) → 𝜒)
21ex 397 . 2 (𝜑 → (𝜓𝜒))
3 impbida.2 . . 3 ((𝜑𝜒) → 𝜓)
43ex 397 . 2 (𝜑 → (𝜒𝜓))
52, 4impbid 202 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382
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  df-an 383
This theorem is referenced by:  eqrdav  2769  frsn  5329  funfvbrb  6473  iinpreima  6488  frnssb  6533  fnprb  6615  fntpb  6616  fpr2g  6618  nvocnv  6679  fsnex  6680  f1prex  6681  f1ocnv2d  7032  el2xptp0  7360  1stconst  7415  2ndconst  7416  cnvf1o  7426  tfrlem15  7640  oeeui  7835  ersymb  7909  swoer  7925  erth  7942  boxriin  8103  boxcutc  8104  domunsncan  8215  pw2f1olem  8219  enen1  8255  enen2  8256  domen1  8257  domen2  8258  sdomen1  8259  sdomen2  8260  xpmapenlem  8282  ordiso2  8575  wdomen1  8636  wdomen2  8637  fin23lem26  9348  fpwwe2lem8  9660  r1wunlim  9760  mul2lt0bi  12138  ixxun  12395  xov1plusxeqvd  12524  fzsplit2  12572  fseq1p1m1  12620  elfz2nn0  12637  flflp1  12815  modsubdir  12946  zesq  13193  hashprg  13383  hashprgOLD  13384  hashgt0elexb  13391  hashbclem  13437  hashge2el2difb  13465  rereb  14067  rlimclim  14484  iserex  14594  caucvgb  14617  mptfzshft  14716  fsumrev  14717  climcnds  14789  fprodrev  14913  dvdsadd2b  15236  nn0ob  15307  bitsfzo  15364  dfgcd2  15470  dvdsmulgcd  15481  lcmgcdeq  15532  qden1elz  15671  mrcidb  16482  mrieqvlemd  16496  isacs2  16520  cicer  16672  ssclem  16685  issubc3  16715  ffthiso  16795  fuciso  16841  setcmon  16943  setcepi  16944  setcinv  16946  catciso  16963  acsfiindd  17384  issstrmgm  17459  issubmnd  17525  mhmf1o  17552  subsubm  17564  resmhm2b  17568  grpinvid1  17677  grpinvid2  17678  subsubg  17824  ssnmz  17843  ghmf1  17896  ghmf1o  17897  conjnmzb  17902  subggim  17915  gicsubgen  17927  gass  17940  odf1  18185  gex1  18212  fislw  18246  sylow3lem2  18249  sylow3lem6  18253  lsmdisj2a  18306  lsmdisj2b  18307  efgred2  18372  dmdprdsplit  18653  0unit  18887  irrednegb  18918  rhmf1o  18941  kerf1hrm  18952  isdrng2  18966  subrgunit  19007  issubdrg  19014  subsubrg  19015  islss3  19171  islss4  19174  lspsnel6  19206  lspsneq0b  19225  islmhm2  19250  lmhmf1o  19258  reslmhm2b  19266  lssvs0or  19322  lvecinv  19325  lspsnel4  19336  lspdisjb  19338  islbs2  19368  islbs3  19369  issubassa  19538  issubassa2  19559  gsumbagdiag  19590  subrgasclcl  19713  prmirredlem  20055  islindf3  20381  lindsmm  20383  lsslindf  20385  lsslinds  20386  matunit  20702  slesolinvbi  20705  en2top  21009  elcls  21097  neindisj2  21147  neiptopnei  21156  neiptopreu  21157  maxlp  21171  neitr  21204  iscncl  21293  cncnp  21304  isreg2  21401  dis2ndc  21483  1stccnp  21485  islly2  21507  dislly  21520  dissnlocfin  21552  kgencmp2  21569  pt1hmeo  21829  xkocnv  21837  t0kq  21841  uffixfr  21946  flimcf  22005  cnpflf2  22023  fclscf  22048  cnextf  22089  utopsnneiplem  22270  isucn2  22302  cfilucfil  22583  psmetutop  22591  restmetu  22594  tngngp2  22675  tngngp  22677  nmoleub  22754  metdseq0  22876  cnheibor  22973  pcophtb  23047  nmoleub2lem  23132  lmmbr  23274  iscfil3  23289  cmetss  23331  cldcss  23430  mbfeqalem  23628  mbfposb  23639  itg2const2  23727  itgss3  23800  plyco0  24167  dgrlt  24241  ulm2  24358  coseq00topi  24474  coseq0negpitopi  24475  sineq0  24493  relogbcxpb  24745  atans2  24878  xrlimcnp  24915  dchrelbas2  25182  dchrn0  25195  2sqb  25377  istrkg2ld  25579  tgcgreqb  25596  tgbtwncomb  25604  trgcgrg  25630  legov  25700  legov2  25701  legov3  25713  hlbtwn  25726  tglineelsb2  25747  tglinecom  25750  colline  25764  mirinv  25781  mirbtwnb  25787  mirbtwnhl  25795  perpcom  25828  isperp2  25830  oppcom  25856  opphllem3  25861  lnopp2hpgb  25875  colopp  25881  colhp  25882  lmieu  25896  iscgra1  25922  dfcgra2  25941  edgnbusgreu  26490  edgnbusgreuOLD  26491  nb3grprlem1  26504  lfgriswlk  26819  eleclclwwlknlem2  27216  clwwlknscsh  27217  clwwlknon1  27269  numclwwlk2lem1  27562  numclwwlk2lem1OLD  27569  grpoinvid1  27716  grpoinvid2  27717  leopmul  29327  hst1h  29420  disjabrex  29727  disjabrexf  29728  erbr3b  29761  f1o3d  29765  funimass4f  29771  fgreu  29805  fcnvgreu  29806  1stpreimas  29817  fcobij  29834  resf1o  29839  fzsplit3  29887  eliccioo  29973  ogrpinv0le  30050  ogrpaddltbi  30053  ogrpaddltrbid  30055  ogrpinv0lt  30057  isarchi3  30075  1smat1  30204  fimaproj  30234  qtophaus  30237  reff  30240  locfinreflem  30241  cmpcref  30251  metider  30271  pstmfval  30273  qqhval2  30360  aean  30641  imambfm  30658  eulerpartlemgvv  30772  orvcgteel  30863  orvclteel  30868  ballotlemsf1o  30909  sgn3da  30937  sgnnbi  30941  sgnpbi  30942  sgnmulsgn  30945  sgnmulsgp  30946  actfunsnf1o  31016  reprsuc  31027  reprpmtf1o  31038  sconnpi1  31553  nosupbnd2  32193  slerec  32254  brofs2  32515  brifs2  32516  broutsideof2  32560  ltflcei  33723  poimirlem25  33760  ismblfin  33776  cnambfre  33783  ftc1anclem6  33815  ismndo1  33997  isdrngo2  34082  lshpnelb  34786  lshpnel2N  34787  lsatspn0  34802  lsatelbN  34808  lsat0cv  34835  lcvexch  34841  lcv1  34843  lkrshp3  34908  lkrpssN  34965  lkrss2N  34971  cvlsupr2  35145  atcvrlln  35321  llncvrlpln  35359  2llnmj  35361  lplncvrlvol  35417  2lplnmj  35423  polcon2bN  35721  pcl0bN  35724  lhpmcvr3  35826  lhpmatb  35832  ltrncoidN  35929  ltrneq3  36010  ltrniotavalbN  36386  cdlemg1cN  36389  diclspsn  36997  dihopelvalcpre  37051  dihord4  37061  dihord  37067  dihmeetlem4preN  37109  dih1dimatlem0  37131  dochsscl  37171  dochoccl  37172  dochord  37173  dochsat  37186  dochshpncl  37187  dochsatshpb  37255  dochshpsat  37257  mapdval4N  37435  mapdsn  37444  hdmap14lem12  37682  hdmapip0  37718  hlhillcs  37761  mrefg2  37789  mzpmfp  37829  lzenom  37852  elpell14qr2  37945  elpell1qr2  37955  pellfund14b  37982  congabseq  38060  acongeq  38069  jm2.23  38082  jm2.20nn  38083  jm2.25lem1  38084  wepwsolem  38131  islssfg2  38160  lnmlmic  38177  dfacbasgrp  38197  rfovcnvf1od  38817  dssmapnvod  38833  ntrclscls00  38883  rfcnpre3  39708  rfcnpre4  39709  rnmptssbi  39989  infxrgelbrnmpt  40193  xnegre  40206  xrpnf  40226  ioossioobi  40256  iccshift  40257  iocopn  40259  eliccelioc  40260  iooshift  40261  icoopn  40264  qinioo  40274  limcdm0  40362  islptre  40363  islpcn  40383  limcresioolb  40387  climuzlem  40487  climlimsup  40504  liminfgelimsup  40526  liminfgelimsupuz  40532  climliminf  40550  climliminflimsup  40552  climliminflimsup2  40553  xlimbr  40565  xlimmnfv  40572  xlimpnfv  40576  xlimclim2  40578  dfxlim2v  40585  fperdvper  40645  itgperiod  40708  fourierdlem32  40867  fourierdlem33  40868  fourierdlem48  40882  fourierdlem49  40883  fourierdlem71  40905  fourierdlem81  40915  smfliminflem  41550  smfliminfmpt  41552  m1mod0mod1  41857  mgmhmf1o  42305  issubmgm2  42308  subsubmgm  42315  resmgmhm2b  42318  rnghmf1o  42421  rngcinv  42499  rngcinvALTV  42511  ringcinv  42550  ringcinvALTV  42574
  Copyright terms: Public domain W3C validator