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

Theorem impbida 872
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 448 . 2 (𝜑 → (𝜓𝜒))
3 impbida.2 . . 3 ((𝜑𝜒) → 𝜓)
43ex 448 . 2 (𝜑 → (𝜒𝜓))
52, 4impbid 200 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  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 195  df-an 384
This theorem is referenced by:  eqrdav  2608  frsn  5102  elsnxpOLD  5581  funfvbrb  6223  iinpreima  6238  frnssb  6283  fnprb  6355  fntpb  6356  fpr2g  6358  nvocnv  6415  fsnex  6416  f1prex  6417  f1ocnv2d  6762  el2xptp0  7081  1stconst  7130  2ndconst  7131  cnvf1o  7141  tfrlem15  7353  oeeui  7547  ersymb  7621  swoer  7637  erth  7656  boxriin  7814  boxcutc  7815  domunsncan  7923  pw2f1olem  7927  enen1  7963  enen2  7964  domen1  7965  domen2  7966  sdomen1  7967  sdomen2  7968  xpmapenlem  7990  ordiso2  8281  wdomen1  8342  wdomen2  8343  fin23lem26  9008  fpwwe2lem8  9316  r1wunlim  9416  mul2lt0bi  11771  ixxun  12021  xov1plusxeqvd  12148  fzsplit2  12195  fseq1p1m1  12241  elfz2nn0  12258  flflp1  12428  modsubdir  12559  zesq  12807  hashprg  12998  hashprgOLD  12999  hashgt0elexb  13006  hashbclem  13048  hashge2el2difb  13072  rereb  13657  rlimclim  14074  iserex  14184  caucvgb  14207  mptfzshft  14301  fsumrev  14302  climcnds  14371  fprodrev  14495  dvdsadd2b  14815  nn0ob  14887  bitsfzo  14944  dfgcd2  15050  dvdsmulgcd  15061  lcmgcdeq  15112  qden1elz  15252  mrcidb  16047  mrieqvlemd  16061  isacs2  16086  cicer  16238  ssclem  16251  issubc3  16281  ffthiso  16361  fuciso  16407  setcmon  16509  setcepi  16510  setcinv  16512  catciso  16529  acsfiindd  16949  issstrmgm  17024  issubmnd  17090  mhmf1o  17117  subsubm  17129  resmhm2b  17133  grpinvid1  17242  grpinvid2  17243  subsubg  17389  ssnmz  17408  ghmf1  17461  ghmf1o  17462  conjnmzb  17467  subggim  17480  gicsubgen  17493  gass  17506  odf1  17751  gex1  17778  fislw  17812  sylow3lem2  17815  sylow3lem6  17819  lsmdisj2a  17872  lsmdisj2b  17873  efgred2  17938  dmdprdsplit  18218  0unit  18452  irrednegb  18483  rhmf1o  18504  kerf1hrm  18515  isdrng2  18529  subrgunit  18570  issubdrg  18577  subsubrg  18578  islss3  18729  islss4  18732  lspsnel6  18764  lspsneq0b  18783  islmhm2  18808  lmhmf1o  18816  reslmhm2b  18824  lssvs0or  18880  lvecinv  18883  lspsnel4  18894  lspdisjb  18896  islbs2  18924  islbs3  18925  issubassa  19094  issubassa2  19115  gsumbagdiag  19146  subrgasclcl  19269  prmirredlem  19608  islindf3  19932  lindsmm  19934  lsslindf  19936  lsslinds  19937  matunit  20251  slesolinvbi  20254  en2top  20548  elcls  20635  neindisj2  20685  neiptopnei  20694  neiptopreu  20695  maxlp  20709  neitr  20742  iscncl  20831  cncnp  20842  isreg2  20939  dis2ndc  21021  1stccnp  21023  islly2  21045  dislly  21058  dissnlocfin  21090  kgencmp2  21107  pt1hmeo  21367  xkocnv  21375  t0kq  21379  uffixfr  21485  flimcf  21544  cnpflf2  21562  fclscf  21587  cnextf  21628  utopsnneiplem  21809  isucn2  21841  cfilucfil  22122  psmetutop  22130  restmetu  22133  tngngp2  22214  tngngp  22216  nmoleub  22293  metdseq0  22413  cnheibor  22510  pcophtb  22585  nmoleub2lem  22670  lmmbr  22809  iscfil3  22824  cmetss  22866  cldcss  22965  mbfeqalem  23160  mbfposb  23171  itg2const2  23259  itgss3  23332  plyco0  23697  dgrlt  23771  ulm2  23888  coseq00topi  24003  coseq0negpitopi  24004  sineq0  24022  relogbcxpb  24270  atans2  24403  xrlimcnp  24440  dchrelbas2  24707  dchrn0  24720  2sqb  24902  istrkg2ld  25104  tgcgreqb  25121  tgbtwncomb  25129  trgcgrg  25156  legov  25226  legov2  25227  legov3  25239  hlbtwn  25252  tglineelsb2  25273  tglinecom  25276  colline  25290  mirinv  25307  mirbtwnb  25313  mirbtwnhl  25321  perpcom  25354  isperp2  25356  oppcom  25382  opphllem3  25387  lnopp2hpgb  25401  colopp  25407  colhp  25408  lmieu  25422  iscgra1  25448  dfcgra2  25467  nb3graprlem1  25774  eleclclwwlknlem2  26140  clwwlknscsh  26141  el2spthonot0  26192  numclwwlk2lem1  26423  grpoinvid1  26560  grpoinvid2  26561  leopmul  28211  hst1h  28304  disjabrex  28611  disjabrexf  28612  erbr3b  28641  f1o3d  28647  funimass4f  28652  fgreu  28688  fcnvgreu  28689  1stpreimas  28700  fcobij  28722  resf1o  28727  fzsplit3  28774  eliccioo  28804  ogrpinv0le  28881  ogrpaddltbi  28884  ogrpaddltrbid  28886  ogrpinv0lt  28888  isarchi3  28906  1smat1  29032  fimaproj  29062  qtophaus  29065  reff  29068  locfinreflem  29069  cmpcref  29079  metider  29099  pstmfval  29101  qqhval2  29188  aean  29468  imambfm  29485  eulerpartlemgvv  29599  orvcgteel  29690  orvclteel  29695  ballotlemsf1o  29736  sgn3da  29764  sgnnbi  29768  sgnpbi  29769  sgnmulsgn  29772  sgnmulsgp  29773  sconpi1  30309  brofs2  31188  brifs2  31189  broutsideof2  31233  ltflcei  32391  poimirlem25  32428  ismblfin  32444  cnambfre  32452  ftc1anclem6  32484  ismndo1  32666  isdrngo2  32751  lshpnelb  33113  lshpnel2N  33114  lsatspn0  33129  lsatelbN  33135  lsat0cv  33162  lcvexch  33168  lcv1  33170  lkrshp3  33235  lkrpssN  33292  lkrss2N  33298  cvlsupr2  33472  atcvrlln  33648  llncvrlpln  33686  2llnmj  33688  lplncvrlvol  33744  2lplnmj  33750  polcon2bN  34048  pcl0bN  34051  lhpmcvr3  34153  lhpmatb  34159  ltrncoidN  34256  ltrneq3  34337  ltrniotavalbN  34714  cdlemg1cN  34717  diclspsn  35325  dihopelvalcpre  35379  dihord4  35389  dihord  35395  dihmeetlem4preN  35437  dih1dimatlem0  35459  dochsscl  35499  dochoccl  35500  dochord  35501  dochsat  35514  dochshpncl  35515  dochsatshpb  35583  dochshpsat  35585  mapdval4N  35763  mapdsn  35772  hdmap14lem12  36013  hdmapip0  36049  hlhillcs  36092  mrefg2  36112  mzpmfp  36152  lzenom  36175  elpell14qr2  36268  elpell1qr2  36278  pellfund14b  36305  congabseq  36383  acongeq  36392  jm2.23  36405  jm2.20nn  36406  jm2.25lem1  36407  wepwsolem  36454  islssfg2  36483  lnmlmic  36500  dfacbasgrp  36521  rfovcnvf1od  37142  dssmapnvod  37158  ntrclscls00  37208  rfcnpre3  38039  rfcnpre4  38040  ioossioobi  38414  iccshift  38415  iocopn  38417  eliccelioc  38418  iooshift  38419  icoopn  38422  qinioo  38433  limcdm0  38509  islptre  38510  islpcn  38530  limcresioolb  38534  fperdvper  38632  itgperiod  38697  fourierdlem32  38856  fourierdlem33  38857  fourierdlem48  38871  fourierdlem49  38872  fourierdlem71  38894  fourierdlem81  38904  m1mod0mod1  39774  edgnbusgreu  40617  nb3grprlem1  40630  lfgriswlk  40919  eleclclwwlksnlem2  41268  clwwlksnscsh  41269  av-numclwwlk2lem1  41554  mgmhmf1o  41599  issubmgm2  41602  subsubmgm  41609  resmgmhm2b  41612  rnghmf1o  41715  rngcinv  41795  rngcinvALTV  41807  ringcinv  41846  ringcinvALTV  41870
  Copyright terms: Public domain W3C validator