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

Theorem impbida 895
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 449 . 2 (𝜑 → (𝜓𝜒))
3 impbida.2 . . 3 ((𝜑𝜒) → 𝜓)
43ex 449 . 2 (𝜑 → (𝜒𝜓))
52, 4impbid 202 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383
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 385
This theorem is referenced by:  eqrdav  2650  frsn  5223  elsnxpOLD  5716  funfvbrb  6370  iinpreima  6385  frnssb  6431  fnprb  6513  fntpb  6514  fpr2g  6516  nvocnv  6577  fsnex  6578  f1prex  6579  f1ocnv2d  6928  el2xptp0  7256  1stconst  7310  2ndconst  7311  cnvf1o  7321  tfrlem15  7533  oeeui  7727  ersymb  7801  swoer  7817  erth  7834  boxriin  7992  boxcutc  7993  domunsncan  8101  pw2f1olem  8105  enen1  8141  enen2  8142  domen1  8143  domen2  8144  sdomen1  8145  sdomen2  8146  xpmapenlem  8168  ordiso2  8461  wdomen1  8522  wdomen2  8523  fin23lem26  9185  fpwwe2lem8  9497  r1wunlim  9597  mul2lt0bi  11974  ixxun  12229  xov1plusxeqvd  12356  fzsplit2  12404  fseq1p1m1  12452  elfz2nn0  12469  flflp1  12648  modsubdir  12779  zesq  13027  hashprg  13220  hashprgOLD  13221  hashgt0elexb  13228  hashbclem  13274  hashge2el2difb  13302  rereb  13904  rlimclim  14321  iserex  14431  caucvgb  14454  mptfzshft  14554  fsumrev  14555  climcnds  14627  fprodrev  14751  dvdsadd2b  15075  nn0ob  15147  bitsfzo  15204  dfgcd2  15310  dvdsmulgcd  15321  lcmgcdeq  15372  qden1elz  15512  mrcidb  16322  mrieqvlemd  16336  isacs2  16361  cicer  16513  ssclem  16526  issubc3  16556  ffthiso  16636  fuciso  16682  setcmon  16784  setcepi  16785  setcinv  16787  catciso  16804  acsfiindd  17224  issstrmgm  17299  issubmnd  17365  mhmf1o  17392  subsubm  17404  resmhm2b  17408  grpinvid1  17517  grpinvid2  17518  subsubg  17664  ssnmz  17683  ghmf1  17736  ghmf1o  17737  conjnmzb  17742  subggim  17755  gicsubgen  17767  gass  17780  odf1  18025  gex1  18052  fislw  18086  sylow3lem2  18089  sylow3lem6  18093  lsmdisj2a  18146  lsmdisj2b  18147  efgred2  18212  dmdprdsplit  18492  0unit  18726  irrednegb  18757  rhmf1o  18780  kerf1hrm  18791  isdrng2  18805  subrgunit  18846  issubdrg  18853  subsubrg  18854  islss3  19007  islss4  19010  lspsnel6  19042  lspsneq0b  19061  islmhm2  19086  lmhmf1o  19094  reslmhm2b  19102  lssvs0or  19158  lvecinv  19161  lspsnel4  19172  lspdisjb  19174  islbs2  19202  islbs3  19203  issubassa  19372  issubassa2  19393  gsumbagdiag  19424  subrgasclcl  19547  prmirredlem  19889  islindf3  20213  lindsmm  20215  lsslindf  20217  lsslinds  20218  matunit  20532  slesolinvbi  20535  en2top  20837  elcls  20925  neindisj2  20975  neiptopnei  20984  neiptopreu  20985  maxlp  20999  neitr  21032  iscncl  21121  cncnp  21132  isreg2  21229  dis2ndc  21311  1stccnp  21313  islly2  21335  dislly  21348  dissnlocfin  21380  kgencmp2  21397  pt1hmeo  21657  xkocnv  21665  t0kq  21669  uffixfr  21774  flimcf  21833  cnpflf2  21851  fclscf  21876  cnextf  21917  utopsnneiplem  22098  isucn2  22130  cfilucfil  22411  psmetutop  22419  restmetu  22422  tngngp2  22503  tngngp  22505  nmoleub  22582  metdseq0  22704  cnheibor  22801  pcophtb  22875  nmoleub2lem  22960  lmmbr  23102  iscfil3  23117  cmetss  23159  cldcss  23258  mbfeqalem  23454  mbfposb  23465  itg2const2  23553  itgss3  23626  plyco0  23993  dgrlt  24067  ulm2  24184  coseq00topi  24299  coseq0negpitopi  24300  sineq0  24318  relogbcxpb  24570  atans2  24703  xrlimcnp  24740  dchrelbas2  25007  dchrn0  25020  2sqb  25202  istrkg2ld  25404  tgcgreqb  25421  tgbtwncomb  25429  trgcgrg  25455  legov  25525  legov2  25526  legov3  25538  hlbtwn  25551  tglineelsb2  25572  tglinecom  25575  colline  25589  mirinv  25606  mirbtwnb  25612  mirbtwnhl  25620  perpcom  25653  isperp2  25655  oppcom  25681  opphllem3  25686  lnopp2hpgb  25700  colopp  25706  colhp  25707  lmieu  25721  iscgra1  25747  dfcgra2  25766  edgnbusgreu  26313  nb3grprlem1  26326  lfgriswlk  26641  eleclclwwlknlem2  27026  clwwlknscsh  27027  clwwlknon1  27072  numclwwlk2lem1  27356  numclwwlk2lem1OLD  27363  grpoinvid1  27510  grpoinvid2  27511  leopmul  29121  hst1h  29214  disjabrex  29521  disjabrexf  29522  erbr3b  29555  f1o3d  29559  funimass4f  29565  fgreu  29599  fcnvgreu  29600  1stpreimas  29611  fcobij  29628  resf1o  29633  fzsplit3  29681  eliccioo  29767  ogrpinv0le  29844  ogrpaddltbi  29847  ogrpaddltrbid  29849  ogrpinv0lt  29851  isarchi3  29869  1smat1  29998  fimaproj  30028  qtophaus  30031  reff  30034  locfinreflem  30035  cmpcref  30045  metider  30065  pstmfval  30067  qqhval2  30154  aean  30435  imambfm  30452  eulerpartlemgvv  30566  orvcgteel  30657  orvclteel  30662  ballotlemsf1o  30703  sgn3da  30731  sgnnbi  30735  sgnpbi  30736  sgnmulsgn  30739  sgnmulsgp  30740  actfunsnf1o  30810  reprsuc  30821  reprpmtf1o  30832  sconnpi1  31347  nosupbnd2  31987  slerec  32048  brofs2  32309  brifs2  32310  broutsideof2  32354  ltflcei  33527  poimirlem25  33564  ismblfin  33580  cnambfre  33588  ftc1anclem6  33620  ismndo1  33802  isdrngo2  33887  lshpnelb  34589  lshpnel2N  34590  lsatspn0  34605  lsatelbN  34611  lsat0cv  34638  lcvexch  34644  lcv1  34646  lkrshp3  34711  lkrpssN  34768  lkrss2N  34774  cvlsupr2  34948  atcvrlln  35124  llncvrlpln  35162  2llnmj  35164  lplncvrlvol  35220  2lplnmj  35226  polcon2bN  35524  pcl0bN  35527  lhpmcvr3  35629  lhpmatb  35635  ltrncoidN  35732  ltrneq3  35813  ltrniotavalbN  36189  cdlemg1cN  36192  diclspsn  36800  dihopelvalcpre  36854  dihord4  36864  dihord  36870  dihmeetlem4preN  36912  dih1dimatlem0  36934  dochsscl  36974  dochoccl  36975  dochord  36976  dochsat  36989  dochshpncl  36990  dochsatshpb  37058  dochshpsat  37060  mapdval4N  37238  mapdsn  37247  hdmap14lem12  37488  hdmapip0  37524  hlhillcs  37567  mrefg2  37587  mzpmfp  37627  lzenom  37650  elpell14qr2  37743  elpell1qr2  37753  pellfund14b  37780  congabseq  37858  acongeq  37867  jm2.23  37880  jm2.20nn  37881  jm2.25lem1  37882  wepwsolem  37929  islssfg2  37958  lnmlmic  37975  dfacbasgrp  37995  rfovcnvf1od  38615  dssmapnvod  38631  ntrclscls00  38681  rfcnpre3  39506  rfcnpre4  39507  rnmptssbi  39791  infxrgelbrnmpt  39996  xnegre  40009  xrpnf  40029  ioossioobi  40061  iccshift  40062  iocopn  40064  eliccelioc  40065  iooshift  40066  icoopn  40069  qinioo  40080  limcdm0  40168  islptre  40169  islpcn  40189  limcresioolb  40193  climuzlem  40293  climlimsup  40310  liminfgelimsup  40332  liminfgelimsupuz  40338  climliminf  40356  climliminflimsup  40358  climliminflimsup2  40359  xlimbr  40371  xlimmnfv  40378  xlimpnfv  40382  xlimclim2  40384  dfxlim2v  40391  fperdvper  40451  itgperiod  40515  fourierdlem32  40674  fourierdlem33  40675  fourierdlem48  40689  fourierdlem49  40690  fourierdlem71  40712  fourierdlem81  40722  smfliminflem  41357  smfliminfmpt  41359  m1mod0mod1  41664  mgmhmf1o  42112  issubmgm2  42115  subsubmgm  42122  resmgmhm2b  42125  rnghmf1o  42228  rngcinv  42306  rngcinvALTV  42318  ringcinv  42357  ringcinvALTV  42381
  Copyright terms: Public domain W3C validator