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

Theorem impbida 800
Description: Deduce an equivalence from two implications. Variant of impbid 211. (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 414 . 2 (𝜑 → (𝜓𝜒))
3 impbida.2 . . 3 ((𝜑𝜒) → 𝜓)
43ex 414 . 2 (𝜑 → (𝜒𝜓))
52, 4impbid 211 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397
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 206  df-an 398
This theorem is referenced by:  biadanid  822  eqrdav  2737  frsn  5716  funfvbrb  6997  iinpreima  7015  fcdmssb  7064  fnprb  7153  fntpb  7154  fpr2g  7156  nvocnv  7222  fsnex  7224  f1ocnv2d  7597  el2xptp0  7959  1stconst  8021  2ndconst  8022  cnvf1o  8032  fimaproj  8056  tfrlem15  8306  oeeui  8517  ersymb  8596  swoer  8612  erth  8631  boxriin  8812  boxcutc  8813  domunsncan  8950  pw2f1olem  8954  enen1  8995  enen2  8996  domen1  8997  domen2  8998  sdomen1  8999  sdomen2  9000  xpmapenlem  9022  ensymfib  9065  ordiso2  9385  wdomen1  9446  wdomen2  9447  fin23lem26  10195  fpwwe2lem7  10507  r1wunlim  10607  mul2lt0bi  12950  ixxun  13209  xov1plusxeqvd  13344  fzsplit2  13395  fseq1p1m1  13444  elfz2nn0  13461  flflp1  13641  modsubdir  13774  zesq  14055  expnngt1b  14071  hashprg  14223  hashgt0elexb  14230  hashbclem  14277  hashge2el2difb  14309  rereb  14939  rlimclim  15363  iserex  15476  caucvgb  15499  mptfzshft  15598  fsumrev  15599  climcnds  15671  fprodrev  15795  dvdsadd2b  16123  nn0ob  16201  bitsfzo  16250  dfgcd2  16362  dvdsmulgcd  16371  lcmgcdeq  16423  qden1elz  16567  mrcidb  17430  mrieqvlemd  17444  isacs2  17468  cicer  17624  ssclem  17637  issubc3  17670  ffthiso  17751  fuciso  17799  setcmon  17908  setcepi  17909  setcinv  17911  catciso  17932  acsfiindd  18377  issstrmgm  18443  issubmnd  18518  mhmf1o  18547  subsubm  18562  resmhm2b  18568  grpinvid1  18736  grpinvid2  18737  subsubg  18884  ssnmz  18901  ghmf1  18970  ghmf1o  18971  conjnmzb  18976  subggim  18989  gicsubgen  19001  gass  19014  odf1  19276  gex1  19303  fislw  19337  sylow3lem2  19340  sylow3lem6  19344  lsmdisj2a  19399  lsmdisj2b  19400  efgred2  19465  dmdprdsplit  19756  2nsgsimpgd  19811  simpgnsgbid  19812  ablsimpgd  19825  0unit  20033  irrednegb  20064  rhmf1o  20088  kerf1ghm  20101  isdrng2  20122  subrgunit  20164  issubdrg  20171  subsubrg  20172  islss3  20344  islss4  20347  lspsnel6  20379  lspsneq0b  20398  islmhm2  20423  lmhmf1o  20431  reslmhm2b  20439  lssvs0or  20495  lvecinv  20498  lspsnel4  20509  lspdisjb  20511  islbs2  20539  islbs3  20540  prmirredlem  20817  islindf3  21156  lindsmm  21158  lsslindf  21160  lsslinds  21161  issubassa  21196  issubassa2  21219  gsumbagdiagOLD  21265  gsumbagdiag  21268  subrgasclcl  21398  matunit  21950  slesolinvbi  21953  en2top  22258  elcls  22347  neindisj2  22397  neiptopnei  22406  neiptopreu  22407  maxlp  22421  neitr  22454  iscncl  22543  cncnp  22554  isreg2  22651  dis2ndc  22734  1stccnp  22736  islly2  22758  dislly  22771  dissnlocfin  22803  kgencmp2  22820  pt1hmeo  23080  xkocnv  23088  t0kq  23092  uffixfr  23197  flimcf  23256  cnpflf2  23274  fclscf  23299  cnextf  23340  utopsnneiplem  23522  isucn2  23554  cfilucfil  23838  psmetutop  23846  restmetu  23849  tngngp2  23939  tngngp  23941  nmoleub  24018  metdseq0  24140  cnheibor  24241  pcophtb  24315  nmoleub2lem  24400  lmmbr  24545  iscfil3  24560  cmetss  24603  cldcss  24728  mbfeqalem2  24929  mbfposb  24940  itg2const2  25029  itgss3  25102  plyco0  25476  dgrlt  25550  ulm2  25667  coseq00topi  25782  coseq0negpitopi  25783  sineq0  25803  relogbcxpb  26060  atans2  26204  xrlimcnp  26241  dchrelbas2  26508  dchrn0  26521  2sqb  26703  nosupbnd2  26987  noinfbnd2  27002  slerec  27081  istrkg2ld  27201  tgcgreqb  27222  tgbtwncomb  27230  trgcgrg  27256  legov  27326  legov2  27327  legov3  27339  hlbtwn  27352  tglineelsb2  27373  tglinecom  27376  colline  27390  mirinv  27407  mirbtwnb  27413  mirbtwnhl  27421  perpcom  27454  isperp2  27456  oppcom  27485  opphllem3  27490  lnopp2hpgb  27504  colopp  27510  colhp  27511  lmieu  27525  iscgra1  27551  dfcgra2  27571  edgnbusgreu  28114  nb3grprlem1  28127  lfgriswlk  28435  eleclclwwlknlem2  28804  clwwlknscsh  28805  clwwlknon1  28840  numclwwlk2lem1  29119  grpoinvid1  29269  grpoinvid2  29270  leopmul  30875  hst1h  30968  diffib  31246  eqsnd  31254  iinabrex  31285  disjabrex  31298  disjabrexf  31299  erbr3b  31334  f1o3d  31339  funimass4f  31349  2ndimaxp  31361  fgreu  31386  fcnvgreu  31387  1stpreimas  31415  fcobij  31434  resf1o  31442  nn0xmulclb  31471  fzsplit3  31492  eliccioo  31582  mgcmntco  31649  dfmgc2lem  31650  dfmgc2  31651  pwrssmgc  31655  mgcf1o  31658  gsumhashmul  31693  ogrpinv0le  31718  ogrpaddltbi  31721  ogrpaddltrbid  31723  ogrpinv0lt  31725  cyc3genpm  31796  isarchi3  31818  prmsimpcyc  31858  qsxpid  31944  grplsmid  31979  quslsm  31980  nsgmgc  31984  nsgqusf1olem2  31986  nsgqusf1olem3  31987  elrspunidl  31993  isprmidlc  32010  prmidl0  32013  qsidom  32017  mxidlnzrb  32031  ply1scleq  32055  lvecdim0  32088  extdg1b  32137  1smat1  32159  ist0cld  32188  qtophaus  32191  reff  32194  locfinreflem  32195  cmpcref  32205  zarcls1  32224  zarclsun  32225  zarclsiin  32226  zarclssn  32228  metider  32249  pstmfval  32251  qqhval2  32337  aean  32617  imambfm  32636  eulerpartlemgvv  32750  orvcgteel  32841  orvclteel  32846  ballotlemsf1o  32887  sgn3da  32915  sgnnbi  32919  sgnpbi  32920  sgnmulsgn  32923  sgnmulsgp  32924  actfunsnf1o  32991  reprsuc  33002  reprpmtf1o  33013  sconnpi1  33607  brofs2  34558  brifs2  34559  broutsideof2  34603  bj-abv  35269  irrdiff  35693  ltflcei  35962  poimirlem25  35999  ismblfin  36015  cnambfre  36022  ftc1anclem6  36052  ismndo1  36228  isdrngo2  36313  eqvrelsymb  36964  eqvrelth  36969  lshpnelb  37342  lshpnel2N  37343  lsatspn0  37358  lsatelbN  37364  lsat0cv  37391  lcvexch  37397  lcv1  37399  lkrshp3  37464  lkrpssN  37521  lkrss2N  37527  cvlsupr2  37701  atcvrlln  37879  llncvrlpln  37917  2llnmj  37919  lplncvrlvol  37975  2lplnmj  37981  polcon2bN  38279  pcl0bN  38282  lhpmcvr3  38384  lhpmatb  38390  ltrncoidN  38487  ltrneq3  38567  ltrniotavalbN  38943  cdlemg1cN  38946  diclspsn  39553  dihopelvalcpre  39607  dihord4  39617  dihord  39623  dihmeetlem4preN  39665  dih1dimatlem0  39687  dochsscl  39727  dochoccl  39728  dochord  39729  dochsat  39742  dochshpncl  39743  dochsatshpb  39811  dochshpsat  39813  mapdval4N  39991  mapdsn  40000  hdmap14lem12  40238  hdmapip0  40274  hlhillcs  40321  riccrng  40605  prjspner1  40830  mrefg2  40896  mzpmfp  40936  lzenom  40959  elpell14qr2  41051  elpell1qr2  41061  pellfund14b  41088  congabseq  41164  acongeq  41173  jm2.23  41186  jm2.20nn  41187  jm2.25lem1  41188  wepwsolem  41235  islssfg2  41264  lnmlmic  41281  dfacbasgrp  41301  rfovcnvf1od  42039  dssmapnvod  42055  ntrclscls00  42103  rfcnpre3  43003  rfcnpre4  43004  rnmptssbi  43248  infxrgelbrnmpt  43448  xnegre  43460  xrpnf  43480  ioossioobi  43510  iccshift  43511  iocopn  43513  eliccelioc  43514  iooshift  43515  icoopn  43518  qinioo  43528  limcdm0  43614  islptre  43615  islpcn  43635  limcresioolb  43639  climuzlem  43739  climlimsup  43756  liminfgelimsup  43778  liminfgelimsupuz  43784  climliminf  43802  climliminflimsup  43804  climliminflimsup2  43805  xlimpnfxnegmnf  43810  xlimbr  43823  xlimmnfv  43830  xlimpnfv  43834  xlimclim2  43836  dfxlim2v  43843  climresdm  43846  xlimresdm  43855  xlimliminflimsup  43858  fperdvper  43915  itgperiod  43977  fourierdlem32  44135  fourierdlem33  44136  fourierdlem48  44150  fourierdlem49  44151  fourierdlem71  44173  fourierdlem81  44183  preimagelt  44695  preimalegt  44696  smfliminflem  44826  smfliminfmpt  44828  fcoresfob  45061  m1mod0mod1  45316  mgmhmf1o  45836  issubmgm2  45839  subsubmgm  45846  resmgmhm2b  45849  rnghmf1o  45956  rngcinv  46034  rngcinvALTV  46046  ringcinv  46085  ringcinvALTV  46109  fvconstr  46677  fvconstrn0  46678  lubeldm2  46744  glbeldm2  46745  functhinclem1  46816  fullthinc  46821  thinciso  46835  prstchom2ALT  46854
  Copyright terms: Public domain W3C validator