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  12951  ixxun  13210  xov1plusxeqvd  13345  fzsplit2  13396  fseq1p1m1  13445  elfz2nn0  13462  flflp1  13642  modsubdir  13775  zesq  14056  expnngt1b  14072  hashprg  14224  hashgt0elexb  14231  hashbclem  14278  hashge2el2difb  14310  rereb  14940  rlimclim  15364  iserex  15477  caucvgb  15500  mptfzshft  15599  fsumrev  15600  climcnds  15672  fprodrev  15796  dvdsadd2b  16124  nn0ob  16202  bitsfzo  16251  dfgcd2  16363  dvdsmulgcd  16372  lcmgcdeq  16424  qden1elz  16568  mrcidb  17431  mrieqvlemd  17445  isacs2  17469  cicer  17625  ssclem  17638  issubc3  17671  ffthiso  17752  fuciso  17800  setcmon  17909  setcepi  17910  setcinv  17912  catciso  17933  acsfiindd  18378  issstrmgm  18444  issubmnd  18519  mhmf1o  18548  subsubm  18563  resmhm2b  18569  grpinvid1  18737  grpinvid2  18738  subsubg  18886  ssnmz  18903  ghmf1  18972  ghmf1o  18973  conjnmzb  18978  subggim  18991  gicsubgen  19003  gass  19016  odf1  19279  gex1  19308  fislw  19342  sylow3lem2  19345  sylow3lem6  19349  lsmdisj2a  19404  lsmdisj2b  19405  efgred2  19470  dmdprdsplit  19761  2nsgsimpgd  19816  simpgnsgbid  19817  ablsimpgd  19830  0unit  20038  irrednegb  20069  rhmf1o  20093  kerf1ghm  20106  isdrng2  20127  subrgunit  20169  issubdrg  20176  subsubrg  20177  islss3  20349  islss4  20352  lspsnel6  20384  lspsneq0b  20403  islmhm2  20428  lmhmf1o  20436  reslmhm2b  20444  lssvs0or  20500  lvecinv  20503  lspsnel4  20514  lspdisjb  20516  islbs2  20544  islbs3  20545  prmirredlem  20822  islindf3  21161  lindsmm  21163  lsslindf  21165  lsslinds  21166  issubassa  21201  issubassa2  21224  gsumbagdiagOLD  21270  gsumbagdiag  21273  subrgasclcl  21403  matunit  21955  slesolinvbi  21958  en2top  22263  elcls  22352  neindisj2  22402  neiptopnei  22411  neiptopreu  22412  maxlp  22426  neitr  22459  iscncl  22548  cncnp  22559  isreg2  22656  dis2ndc  22739  1stccnp  22741  islly2  22763  dislly  22776  dissnlocfin  22808  kgencmp2  22825  pt1hmeo  23085  xkocnv  23093  t0kq  23097  uffixfr  23202  flimcf  23261  cnpflf2  23279  fclscf  23304  cnextf  23345  utopsnneiplem  23527  isucn2  23559  cfilucfil  23843  psmetutop  23851  restmetu  23854  tngngp2  23944  tngngp  23946  nmoleub  24023  metdseq0  24145  cnheibor  24246  pcophtb  24320  nmoleub2lem  24405  lmmbr  24550  iscfil3  24565  cmetss  24608  cldcss  24733  mbfeqalem2  24934  mbfposb  24945  itg2const2  25034  itgss3  25107  plyco0  25481  dgrlt  25555  ulm2  25672  coseq00topi  25787  coseq0negpitopi  25788  sineq0  25808  relogbcxpb  26065  atans2  26209  xrlimcnp  26246  dchrelbas2  26513  dchrn0  26526  2sqb  26708  nosupbnd2  26992  noinfbnd2  27007  slerec  27086  istrkg2ld  27207  tgcgreqb  27228  tgbtwncomb  27236  trgcgrg  27262  legov  27332  legov2  27333  legov3  27345  hlbtwn  27358  tglineelsb2  27379  tglinecom  27382  colline  27396  mirinv  27413  mirbtwnb  27419  mirbtwnhl  27427  perpcom  27460  isperp2  27462  oppcom  27491  opphllem3  27496  lnopp2hpgb  27510  colopp  27516  colhp  27517  lmieu  27531  iscgra1  27557  dfcgra2  27577  edgnbusgreu  28120  nb3grprlem1  28133  lfgriswlk  28441  eleclclwwlknlem2  28810  clwwlknscsh  28811  clwwlknon1  28846  numclwwlk2lem1  29125  grpoinvid1  29275  grpoinvid2  29276  leopmul  30881  hst1h  30974  diffib  31252  eqsnd  31260  iinabrex  31291  disjabrex  31304  disjabrexf  31305  erbr3b  31340  f1o3d  31345  funimass4f  31355  2ndimaxp  31367  fgreu  31392  fcnvgreu  31393  1stpreimas  31421  fcobij  31440  resf1o  31448  nn0xmulclb  31477  fzsplit3  31498  eliccioo  31588  mgcmntco  31655  dfmgc2lem  31656  dfmgc2  31657  pwrssmgc  31661  mgcf1o  31664  gsumhashmul  31699  ogrpinv0le  31724  ogrpaddltbi  31727  ogrpaddltrbid  31729  ogrpinv0lt  31731  cyc3genpm  31802  isarchi3  31824  prmsimpcyc  31864  qsxpid  31950  grplsmid  31985  quslsm  31986  nsgmgc  31990  nsgqusf1olem2  31992  nsgqusf1olem3  31993  elrspunidl  31999  isprmidlc  32016  prmidl0  32019  qsidom  32023  mxidlnzrb  32037  ply1scleq  32061  lvecdim0  32094  extdg1b  32143  1smat1  32165  ist0cld  32194  qtophaus  32197  reff  32200  locfinreflem  32201  cmpcref  32211  zarcls1  32230  zarclsun  32231  zarclsiin  32232  zarclssn  32234  metider  32255  pstmfval  32257  qqhval2  32343  aean  32623  imambfm  32642  eulerpartlemgvv  32756  orvcgteel  32847  orvclteel  32852  ballotlemsf1o  32893  sgn3da  32921  sgnnbi  32925  sgnpbi  32926  sgnmulsgn  32929  sgnmulsgp  32930  actfunsnf1o  32997  reprsuc  33008  reprpmtf1o  33019  sconnpi1  33613  brofs2  34593  brifs2  34594  broutsideof2  34638  bj-abv  35304  irrdiff  35728  ltflcei  35997  poimirlem25  36034  ismblfin  36050  cnambfre  36057  ftc1anclem6  36087  ismndo1  36263  isdrngo2  36348  eqvrelsymb  36999  eqvrelth  37004  lshpnelb  37377  lshpnel2N  37378  lsatspn0  37393  lsatelbN  37399  lsat0cv  37426  lcvexch  37432  lcv1  37434  lkrshp3  37499  lkrpssN  37556  lkrss2N  37562  cvlsupr2  37736  atcvrlln  37914  llncvrlpln  37952  2llnmj  37954  lplncvrlvol  38010  2lplnmj  38016  polcon2bN  38314  pcl0bN  38317  lhpmcvr3  38419  lhpmatb  38425  ltrncoidN  38522  ltrneq3  38602  ltrniotavalbN  38978  cdlemg1cN  38981  diclspsn  39588  dihopelvalcpre  39642  dihord4  39652  dihord  39658  dihmeetlem4preN  39700  dih1dimatlem0  39722  dochsscl  39762  dochoccl  39763  dochord  39764  dochsat  39777  dochshpncl  39778  dochsatshpb  39846  dochshpsat  39848  mapdval4N  40026  mapdsn  40035  hdmap14lem12  40273  hdmapip0  40309  hlhillcs  40356  riccrng  40638  prjspner1  40866  mrefg2  40932  mzpmfp  40972  lzenom  40995  elpell14qr2  41087  elpell1qr2  41097  pellfund14b  41124  congabseq  41200  acongeq  41209  jm2.23  41222  jm2.20nn  41223  jm2.25lem1  41224  wepwsolem  41271  islssfg2  41300  lnmlmic  41317  dfacbasgrp  41337  rfovcnvf1od  42075  dssmapnvod  42091  ntrclscls00  42139  rfcnpre3  43039  rfcnpre4  43040  rnmptssbi  43284  infxrgelbrnmpt  43484  xnegre  43496  xrpnf  43516  ioossioobi  43546  iccshift  43547  iocopn  43549  eliccelioc  43550  iooshift  43551  icoopn  43554  qinioo  43564  limcdm0  43650  islptre  43651  islpcn  43671  limcresioolb  43675  climuzlem  43775  climlimsup  43792  liminfgelimsup  43814  liminfgelimsupuz  43820  climliminf  43838  climliminflimsup  43840  climliminflimsup2  43841  xlimpnfxnegmnf  43846  xlimbr  43859  xlimmnfv  43866  xlimpnfv  43870  xlimclim2  43872  dfxlim2v  43879  climresdm  43882  xlimresdm  43891  xlimliminflimsup  43894  fperdvper  43951  itgperiod  44013  fourierdlem32  44171  fourierdlem33  44172  fourierdlem48  44186  fourierdlem49  44187  fourierdlem71  44209  fourierdlem81  44219  preimagelt  44731  preimalegt  44732  smfliminflem  44862  smfliminfmpt  44864  fcoresfob  45097  m1mod0mod1  45352  mgmhmf1o  45872  issubmgm2  45875  subsubmgm  45882  resmgmhm2b  45885  rnghmf1o  45992  rngcinv  46070  rngcinvALTV  46082  ringcinv  46121  ringcinvALTV  46145  fvconstr  46713  fvconstrn0  46714  lubeldm2  46780  glbeldm2  46781  functhinclem1  46852  fullthinc  46857  thinciso  46871  prstchom2ALT  46890
  Copyright terms: Public domain W3C validator