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

Theorem impbida 876
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 450 . 2 (𝜑 → (𝜓𝜒))
3 impbida.2 . . 3 ((𝜑𝜒) → 𝜓)
43ex 450 . 2 (𝜑 → (𝜒𝜓))
52, 4impbid 202 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384
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 386
This theorem is referenced by:  eqrdav  2619  frsn  5179  elsnxpOLD  5666  funfvbrb  6316  iinpreima  6331  frnssb  6377  fnprb  6457  fntpb  6458  fpr2g  6460  nvocnv  6522  fsnex  6523  f1prex  6524  f1ocnv2d  6871  el2xptp0  7197  1stconst  7250  2ndconst  7251  cnvf1o  7261  tfrlem15  7473  oeeui  7667  ersymb  7741  swoer  7757  erth  7776  boxriin  7935  boxcutc  7936  domunsncan  8045  pw2f1olem  8049  enen1  8085  enen2  8086  domen1  8087  domen2  8088  sdomen1  8089  sdomen2  8090  xpmapenlem  8112  ordiso2  8405  wdomen1  8466  wdomen2  8467  fin23lem26  9132  fpwwe2lem8  9444  r1wunlim  9544  mul2lt0bi  11921  ixxun  12176  xov1plusxeqvd  12303  fzsplit2  12351  fseq1p1m1  12398  elfz2nn0  12415  flflp1  12591  modsubdir  12722  zesq  12970  hashprg  13165  hashprgOLD  13166  hashgt0elexb  13173  hashbclem  13219  hashge2el2difb  13247  rereb  13841  rlimclim  14258  iserex  14368  caucvgb  14391  mptfzshft  14491  fsumrev  14492  climcnds  14564  fprodrev  14688  dvdsadd2b  15009  nn0ob  15081  bitsfzo  15138  dfgcd2  15244  dvdsmulgcd  15255  lcmgcdeq  15306  qden1elz  15446  mrcidb  16256  mrieqvlemd  16270  isacs2  16295  cicer  16447  ssclem  16460  issubc3  16490  ffthiso  16570  fuciso  16616  setcmon  16718  setcepi  16719  setcinv  16721  catciso  16738  acsfiindd  17158  issstrmgm  17233  issubmnd  17299  mhmf1o  17326  subsubm  17338  resmhm2b  17342  grpinvid1  17451  grpinvid2  17452  subsubg  17598  ssnmz  17617  ghmf1  17670  ghmf1o  17671  conjnmzb  17676  subggim  17689  gicsubgen  17702  gass  17715  odf1  17960  gex1  17987  fislw  18021  sylow3lem2  18024  sylow3lem6  18028  lsmdisj2a  18081  lsmdisj2b  18082  efgred2  18147  dmdprdsplit  18427  0unit  18661  irrednegb  18692  rhmf1o  18713  kerf1hrm  18724  isdrng2  18738  subrgunit  18779  issubdrg  18786  subsubrg  18787  islss3  18940  islss4  18943  lspsnel6  18975  lspsneq0b  18994  islmhm2  19019  lmhmf1o  19027  reslmhm2b  19035  lssvs0or  19091  lvecinv  19094  lspsnel4  19105  lspdisjb  19107  islbs2  19135  islbs3  19136  issubassa  19305  issubassa2  19326  gsumbagdiag  19357  subrgasclcl  19480  prmirredlem  19822  islindf3  20146  lindsmm  20148  lsslindf  20150  lsslinds  20151  matunit  20465  slesolinvbi  20468  en2top  20770  elcls  20858  neindisj2  20908  neiptopnei  20917  neiptopreu  20918  maxlp  20932  neitr  20965  iscncl  21054  cncnp  21065  isreg2  21162  dis2ndc  21244  1stccnp  21246  islly2  21268  dislly  21281  dissnlocfin  21313  kgencmp2  21330  pt1hmeo  21590  xkocnv  21598  t0kq  21602  uffixfr  21708  flimcf  21767  cnpflf2  21785  fclscf  21810  cnextf  21851  utopsnneiplem  22032  isucn2  22064  cfilucfil  22345  psmetutop  22353  restmetu  22356  tngngp2  22437  tngngp  22439  nmoleub  22516  metdseq0  22638  cnheibor  22735  pcophtb  22810  nmoleub2lem  22895  lmmbr  23037  iscfil3  23052  cmetss  23094  cldcss  23193  mbfeqalem  23390  mbfposb  23401  itg2const2  23489  itgss3  23562  plyco0  23929  dgrlt  24003  ulm2  24120  coseq00topi  24235  coseq0negpitopi  24236  sineq0  24254  relogbcxpb  24506  atans2  24639  xrlimcnp  24676  dchrelbas2  24943  dchrn0  24956  2sqb  25138  istrkg2ld  25340  tgcgreqb  25357  tgbtwncomb  25365  trgcgrg  25391  legov  25461  legov2  25462  legov3  25474  hlbtwn  25487  tglineelsb2  25508  tglinecom  25511  colline  25525  mirinv  25542  mirbtwnb  25548  mirbtwnhl  25556  perpcom  25589  isperp2  25591  oppcom  25617  opphllem3  25622  lnopp2hpgb  25636  colopp  25642  colhp  25643  lmieu  25657  iscgra1  25683  dfcgra2  25702  edgnbusgreu  26250  nb3grprlem1  26263  lfgriswlk  26566  eleclclwwlksnlem2  26919  clwwlksnscsh  26920  numclwwlk2lem1  27206  grpoinvid1  27352  grpoinvid2  27353  leopmul  28963  hst1h  29056  disjabrex  29367  disjabrexf  29368  erbr3b  29399  f1o3d  29404  funimass4f  29410  fgreu  29445  fcnvgreu  29446  1stpreimas  29457  fcobij  29474  resf1o  29479  fzsplit3  29527  eliccioo  29613  ogrpinv0le  29690  ogrpaddltbi  29693  ogrpaddltrbid  29695  ogrpinv0lt  29697  isarchi3  29715  1smat1  29844  fimaproj  29874  qtophaus  29877  reff  29880  locfinreflem  29881  cmpcref  29891  metider  29911  pstmfval  29913  qqhval2  30000  aean  30281  imambfm  30298  eulerpartlemgvv  30412  orvcgteel  30503  orvclteel  30508  ballotlemsf1o  30549  sgn3da  30577  sgnnbi  30581  sgnpbi  30582  sgnmulsgn  30585  sgnmulsgp  30586  actfunsnf1o  30656  reprsuc  30667  reprpmtf1o  30678  sconnpi1  31195  nosupbnd2  31836  slerec  31897  brofs2  32159  brifs2  32160  broutsideof2  32204  ltflcei  33368  poimirlem25  33405  ismblfin  33421  cnambfre  33429  ftc1anclem6  33461  ismndo1  33643  isdrngo2  33728  lshpnelb  34090  lshpnel2N  34091  lsatspn0  34106  lsatelbN  34112  lsat0cv  34139  lcvexch  34145  lcv1  34147  lkrshp3  34212  lkrpssN  34269  lkrss2N  34275  cvlsupr2  34449  atcvrlln  34625  llncvrlpln  34663  2llnmj  34665  lplncvrlvol  34721  2lplnmj  34727  polcon2bN  35025  pcl0bN  35028  lhpmcvr3  35130  lhpmatb  35136  ltrncoidN  35233  ltrneq3  35314  ltrniotavalbN  35691  cdlemg1cN  35694  diclspsn  36302  dihopelvalcpre  36356  dihord4  36366  dihord  36372  dihmeetlem4preN  36414  dih1dimatlem0  36436  dochsscl  36476  dochoccl  36477  dochord  36478  dochsat  36491  dochshpncl  36492  dochsatshpb  36560  dochshpsat  36562  mapdval4N  36740  mapdsn  36749  hdmap14lem12  36990  hdmapip0  37026  hlhillcs  37069  mrefg2  37089  mzpmfp  37129  lzenom  37152  elpell14qr2  37245  elpell1qr2  37255  pellfund14b  37282  congabseq  37360  acongeq  37369  jm2.23  37382  jm2.20nn  37383  jm2.25lem1  37384  wepwsolem  37431  islssfg2  37460  lnmlmic  37477  dfacbasgrp  37497  rfovcnvf1od  38118  dssmapnvod  38134  ntrclscls00  38184  rfcnpre3  39012  rfcnpre4  39013  rnmptssbi  39293  infxrgelbrnmpt  39496  xnegre  39509  ioossioobi  39546  iccshift  39547  iocopn  39549  eliccelioc  39550  iooshift  39551  icoopn  39554  qinioo  39565  limcdm0  39650  islptre  39651  islpcn  39671  limcresioolb  39675  climuzlem  39775  climlimsup  39786  liminfgelimsup  39808  liminfgelimsupuz  39814  climliminf  39832  climliminflimsup  39834  climliminflimsup2  39835  fperdvper  39896  itgperiod  39960  fourierdlem32  40119  fourierdlem33  40120  fourierdlem48  40134  fourierdlem49  40135  fourierdlem71  40157  fourierdlem81  40167  smfliminflem  40799  smfliminfmpt  40801  m1mod0mod1  41103  mgmhmf1o  41552  issubmgm2  41555  subsubmgm  41562  resmgmhm2b  41565  rnghmf1o  41668  rngcinv  41746  rngcinvALTV  41758  ringcinv  41797  ringcinvALTV  41821
  Copyright terms: Public domain W3C validator