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

Theorem impbid 213
Description: Deduce an equivalence from two implications. Deduction associated with impbi 209 and impbii 210. (Contributed by NM, 24-Jan-1993.) Revised to prove it from impbid21d 212. (Revised by Wolf Lammen, 3-Nov-2012.)
Hypotheses
Ref Expression
impbid.1 (𝜑 → (𝜓𝜒))
impbid.2 (𝜑 → (𝜒𝜓))
Assertion
Ref Expression
impbid (𝜑 → (𝜓𝜒))

Proof of Theorem impbid
StepHypRef Expression
1 impbid.1 . . 3 (𝜑 → (𝜓𝜒))
2 impbid.2 . . 3 (𝜑 → (𝜒𝜓))
31, 2impbid21d 212 . 2 (𝜑 → (𝜑 → (𝜓𝜒)))
43pm2.43i 52 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207
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 208
This theorem is referenced by:  bicom1  222  impbid1  226  impcon4bid  228  pm5.74  271  imbi1d  343  pm5.501  368  2falsed  378  impbida  797  dedlem0b  1036  dedlema  1037  dedlemb  1038  albi  1810  alexbii  1824  equequ1  2023  equequ2  2024  spsbbi  2069  sbbidvOLD  2076  sbequOLD  2083  elequ1  2112  elequ2  2120  sbbidOLD  2239  sbequ12  2244  sbft  2261  sb56OLD  2270  sbequvvOLD  2327  cbv2w  2349  exsb  2371  dral1v  2380  cbv2  2417  cbv2h  2420  ax12b  2441  dral1  2456  dral1ALT  2457  sbequ12ALT  2577  sbftALT  2589  sbequALT  2593  eupickb  2716  eupickbi  2717  2eu2  2734  ralbi  3167  ceqsalt  3528  vtoclgft  3554  rspcebdv  3616  ceqex  3644  mob2  3705  reu6  3716  sbciegft  3807  2reu2  3881  csbiebt  3911  sseq1  3991  ssdifsym  4239  reupick  4286  reupick2  4288  uneqdifeq  4436  prnebg  4780  preqsnd  4783  prel12g  4788  disjeq2  5027  disjeq1  5030  disjss3  5057  reusv2lem2  5291  reusv2lem3  5292  alxfr  5299  ralxfrd  5300  ralxfrd2  5304  copsexgw  5373  copsexg  5374  snopeqop  5388  euotd  5395  poeq2  5472  sotric  5495  sotrieq  5496  freq2  5520  seeq1  5521  seeq2  5522  iss  5897  tz7.7  6211  ordtri1  6218  ordelinel  6283  iotaval  6323  funeq  6369  funssres  6392  f0dom0  6557  tz6.12c  6689  fnbrfvb  6712  ssimaex  6742  fvimacnv  6816  elpreima  6821  eldmrexrnb  6851  fsn  6890  fnsnb  6921  fmptsng  6923  fmptsnd  6924  fprb  6949  tpres  6956  fconst2g  6958  fconst5  6961  elunirn  7001  f1ocnvfvb  7027  f1prex  7031  foeqcnvco  7047  f1eqcocnv  7048  fliftfun  7054  soisores  7069  isofr  7084  isose  7085  isopo  7088  isoso  7090  f1oiso2  7094  eusvobj2  7138  oprabidw  7176  oprabid  7177  f1opw2  7389  oneqmin  7508  ordsuc  7517  ordelsuc  7523  ordsucelsuc  7525  ordunisuc2  7547  limsuc  7552  f1ovv  7650  op1steq  7724  opreuopreu  7725  funeldmdif  7738  fvn0elsuppb  7838  extmptsuppeq  7845  rntpos  7896  smoiso2  7997  seqomlem2  8078  oaord  8163  oawordex  8173  oaordex  8174  omord2  8183  om00  8191  oeord  8204  nnaord  8235  nnmord  8248  nnawordex  8253  nnaordex  8254  erexb  8304  swoord1  8310  swoord2  8311  iiner  8359  eceqoveq  8392  mapsnd  8439  ralxpmap  8449  omxpenlem  8607  domtriord  8652  mapxpen  8672  mapunen  8675  ssenen  8680  nneneq  8689  onomeneq  8697  nndomo  8701  en1eqsnbi  8738  fodomfib  8787  f1opwfi  8817  fsuppunbi  8843  elfiun  8883  suplub2  8914  ordiso2  8968  ordiso  8969  oieu  8992  brwdom2  9026  brwdom3  9035  cantnflem1  9141  cardidm  9377  carddom2  9395  pm54.43  9418  pr2ne  9420  acnen  9468  acnen2  9470  alephord  9490  alephinit  9510  dfac5  9543  infdif2  9621  fictb  9656  coflim  9672  fincssdom  9734  fin23lem25  9735  isf32lem9  9772  isf34lem4  9788  fin1a2lem11  9821  axdc3lem2  9862  ficard  9976  fpwwe2lem12  10052  fpwwe2  10054  indpi  10318  nqereq  10346  1idpr  10440  ltapr  10456  leltne  10719  ltlen  10730  ltadd2  10733  addlsub  11045  addid0  11048  ltord1  11155  mul0or  11269  ldiv  11463  ltmul1  11479  mulge0b  11499  lt2msq  11514  negfi  11578  nnsub  11670  nn0sub  11936  zrevaddcl  12016  zltp1le  12021  zdiv  12041  nneo  12055  zeo2  12058  zmax  12334  zbtwnre  12335  qrevaddcl  12360  xrlttri  12522  xrleltne  12528  xralrple  12588  xltneg  12600  xleadd1  12638  xlemul1  12673  supxrunb1  12702  supxrunb2  12703  ioo0  12753  iccid  12773  ico0  12774  ioc0  12775  icc0  12776  difreicc  12860  iccsplit  12861  zltaddlt1le  12880  0fz1  12917  uzsplit  12969  fzm1  12977  fzrevral  12982  ssfzo12bi  13122  elfznelfzob  13133  flge  13165  modid2  13256  modmuladd  13271  ssnn0fi  13343  seqf1olem1  13399  hashen  13697  hashdom  13730  hash2exprb  13819  pr2pwpr  13827  hashtpg  13833  len0nnbi  13893  ccats1pfxeqbi  14094  reuccatpfxs1  14099  repsdf2  14130  scshwfzeqfzo  14178  relexpindlem  14412  shftlem  14417  shftuz  14418  abslt  14664  absle  14665  rexico  14703  cau3lem  14704  reusq0  14812  rlim2lt  14844  rlim3  14845  o1lo1  14884  rlimdm  14898  climshft  14923  o1dif  14976  isercolllem2  15012  isercoll  15014  zsum  15065  fsum  15067  fsum00  15143  incexclem  15181  zprod  15281  fprod  15285  dvdsval2  15600  moddvds  15608  negdvdsb  15616  dvdsnegb  15617  dvdscmulr  15628  dvdsmulcr  15629  dvdssub2  15641  dvdsaddre2b  15647  fzo0dvdseq  15663  mod2eq1n2dvds  15686  ltoddhalfle  15700  sumodd  15729  bitsf1ocnv  15783  sadcaddlem  15796  bitsuz  15813  dvdsgcdb  15883  gcdzeq  15892  dvdssqlem  15900  lcmeq0  15934  lcmdvdsb  15947  lcmfeq0b  15964  lcmf  15967  lcmfdvdsb  15977  coprmgcdb  15983  cncongr  16003  isprm2lem  16015  dvdsprime  16021  dvdsprm  16037  isprm7  16042  coprm  16045  euclemma  16047  rpexp  16054  prmdiveq  16113  hashgcdlem  16115  odzdvds  16122  pythagtrip  16161  pc2dvds  16205  pcprmpw2  16208  pcprmpw  16209  vdwapun  16300  ramtcl2  16337  firest  16696  mrieqv2d  16900  isacs2  16914  isssc  17080  setciso  17341  posasymb  17552  pleval2  17565  pltval3  17567  lublecllem  17588  joinle  17614  meetle  17628  lubun  17723  clatleglb  17726  latdisd  17790  letsr  17827  intopsn  17854  gsumval2a  17885  frmdss2  18018  isgrpid2  18080  isgrpinv  18096  symg1bas  18455  oddvdsnn0  18603  oddvds  18606  odeq  18609  odeq1  18618  gexdvds  18640  pgpfi  18661  pgpssslw  18670  fislw  18681  sylow3lem2  18684  lsmelvalm  18707  lsmlub  18721  lsmss1b  18723  lsmss2b  18725  efgs1b  18793  cyggenod  18934  cyggexb  18950  dprdfeq0  19075  ablsimpgfind  19163  ringinvnz1ne0  19273  ringinvnzdiv  19274  unitmulclb  19346  dvreq1  19374  f1ghm0to0  19423  f1rhm0to0OLD  19424  f1rhm0to0ALT  19425  drngmul0or  19454  isabvd  19522  issrngd  19563  lssats2  19703  lspsneq0  19715  lsmelval2  19788  lvecvs0or  19811  lspsneq  19825  lspsneu  19826  lidl1el  19921  lidldvgen  19958  isnzr2  19966  0ringnnzr  19972  0ring01eqbi  19976  rrgeq0  19993  domneq0  20000  ply1coe1eq  20396  cply1coe0bi  20398  znunit  20640  psgndif  20676  ipeq0  20712  ocvsscon  20749  pjdm2  20785  obselocv  20802  islinds4  20909  mat1dimelbas  21010  cramer  21230  toponcomb  21467  tgss3  21524  clsval2  21588  isopn3  21604  elcls3  21621  opncldf1  21622  neiint  21642  neips  21651  opnneissb  21652  opnssneib  21653  opnnei  21658  tpnei  21659  opnneiid  21664  restcld  21710  restopnb  21713  tgcn  21790  tgcnp  21791  subbascn  21792  iscnp4  21801  cnpnei  21802  cncls2  21811  cncls  21812  cnntr  21813  lmss  21836  hausnei2  21891  lpcls  21902  ordtt1  21917  cmpsub  21938  tgcmp  21939  1stcelcls  21999  locfincmp  22064  kgencn2  22095  ptpjpre1  22109  upxp  22161  txcn  22164  txlm  22186  tgqtop  22250  kqfvima  22268  isr0  22275  regr1lem2  22278  hmeoopn  22304  hmeocld  22305  ptuncnv  22345  fbunfip  22407  fgss2  22412  ufilb  22444  ufprim  22447  trufil  22448  cfinufil  22466  ufildr  22469  elfm2  22486  elfm3  22488  rnelfm  22491  fmfnfmlem4  22495  fmco  22499  flimtopon  22508  flimopn  22513  fbflim2  22515  flimrest  22521  flffbas  22533  cnpflf  22539  fclstopon  22550  fclsnei  22557  fclsbas  22559  fclsfnflim  22565  fclscmp  22568  ufilcmp  22570  isfcf  22572  fcfnei  22573  cnpfcf  22579  alexsubb  22584  alexsubALT  22589  cldsubg  22648  tgphaus  22654  tgpt0  22656  tsmsgsum  22676  tsmsres  22681  xbln0  22953  blssexps  22965  blssex  22966  isxms2  22987  prdsbl  23030  neibl  23040  metss  23047  met2ndc  23062  metrest  23063  metcnp3  23079  tngngp3  23194  nmoeq0  23274  xrsxmet  23346  reconn  23365  iccpnfcnv  23477  fgcfil  23803  iscau4  23811  cfilres  23828  iunmbl2  24087  ismbf3d  24184  mbfaddlem  24190  i1faddlem  24223  i1fmullem  24224  ellimc3  24406  tdeglem4  24583  deg1nn0clb  24613  deg1lt0  24614  dvdsq1p  24683  plypf1  24731  0dgrb  24765  plymul0or  24799  ulmshft  24907  ulmcaulem  24911  ulmcau  24912  cosord  25043  eff1olem  25059  lognegb  25100  eflogeq  25112  logdivlt  25131  efopn  25168  cxpeq0  25188  cxpeq  25265  angpieqvd  25336  dcubic  25351  asinsinb  25402  acoscosb  25403  atantanb  25429  rlimcnp  25471  isppw  25619  isppw2  25620  vmappw  25621  isnsqf  25640  ppieq0  25681  fsumdvdsdiag  25689  dvdsppwf1o  25691  fsumfldivdiag  25695  chpeq0  25712  chteq0  25713  dchrptlem1  25768  lgsdir2lem4  25832  lgsne0  25839  lgsqr  25855  lgsdchrval  25858  gausslemma2dlem1a  25869  lgsquadlem1  25884  m1lgs  25892  2sqreultblem  25952  2sqreunnltblem  25955  iscgrglt  26228  brbtwn  26613  brcgr  26614  brbtwn2  26619  axcontlem7  26684  uhgr0vb  26785  edglnl  26856  ausgrusgrb  26878  ushgredgedg  26939  ushgredgedgloop  26941  usgr0vb  26947  usgr1v  26966  nbupgr  27054  nbumgrvtx  27056  nbuhgr2vtx1edgb  27062  edgusgrnbfin  27083  nb3grprlem1  27090  uvtxnbvtxm1  27116  cusgrfilem2  27166  uhgr0edg0rgrb  27284  cusgrm1rusgr  27292  spthonepeq  27461  usgr2pth  27473  wlkiswwlks  27582  wlkiswwlkupgr  27584  wlklnwwlkn  27590  wlklnwwlknupgr  27592  wwlksnextbi  27600  wwlksnredwwlkn0  27602  wwlksnextwrd  27603  wwlksnextprop  27619  umgrwwlks2on  27664  elwspths2on  27667  usgr2wspthons3  27671  elwwlks2  27673  elwspths2spth  27674  clwlkclwwlklem3  27707  loopclwwlkn1b  27748  clwwlknon1sn  27807  clwwlknonwwlknonb  27813  umgr3v3e3cycl  27891  eupth2lem3lem4  27938  frgr0v  27969  frgr3vlem2  27981  2clwwlk2clwwlk  28057  wlkl0  28074  grpoinvf  28237  nvmul0or  28355  nvz  28374  diporthcom  28421  ubthlem3  28577  hvmul0or  28730  his6  28804  hial0  28807  hial02  28808  orthcom  28813  normgt0  28832  ocin  29001  occon3  29002  shsel3  29020  shlub  29119  chssoc  29201  h1de2bi  29259  spansncol  29273  elspansn4  29278  spansnss2  29280  sumspansn  29354  lnopcnbd  29741  lnfncnbd  29762  riesz1  29770  elpjrn  29895  cvcon3  29989  dmdmd  30005  dmdbr3  30010  dmdbr4  30011  dmdbr5  30013  mdslmd1i  30034  atcveq0  30053  chcv1  30060  atssma  30083  atcv0eq  30084  atcv1  30085  bian1d  30152  disjeq1f  30252  br8d  30290  fpwrelmap  30396  xaddeq0  30404  eliccelico  30427  elicoelioo  30428  isarchiofld  30818  unitdivcld  31044  xrge0iifcnv  31076  lmxrge0  31095  indf1ofs  31185  eulerpartlemgh  31536  dstfrvunirn  31632  loop1cycl  32282  cusgracyclt3v  32301  cvmliftmolem2  32427  cvmlift2lem12  32459  satfvsucsuc  32510  satfdm  32514  fmlasuc  32531  satffunlem1lem2  32548  satffunlem2lem2  32551  mthmb  32726  climuzcnv  32812  br8  32890  br6  32891  br4  32892  funbreq  32911  axextbdist  32943  nodenselem8  33093  dfrdg4  33310  cgrcom  33349  cgrcoml  33355  cgrdegen  33363  btwncom  33373  brsegle  33467  brsegle2  33468  colinbtwnle  33477  btwnoutside  33484  broutsideof3  33485  outsidele  33491  lineunray  33506  lineelsb2  33507  elhf2  33534  elicc3  33563  nn0prpwlem  33568  opnbnd  33571  cldbnd  33572  opnregcld  33576  cldregopn  33577  fnessref  33603  refssfne  33604  neibastop2  33607  fnemeet2  33613  fnejoin2  33615  fgmin  33616  ontgval  33677  ordtop  33682  ordcmp  33693  nndivsub  33703  bj-19.21t  33996  bj-19.23t  33997  bj-19.42t  34000  bj-sbft  34002  bj-cbv2hv  34017  bj-equsal1t  34043  bj-19.21t0  34051  bj-ceqsalt0  34098  bj-ceqsalt1  34099  bj-xpnzexb  34171  bj-idreseq  34347  bj-finsumval0  34456  bj-fvimacnv0  34457  bj-isrvec2  34470  bj-bary1  34482  dfgcd3  34488  isbasisrelowllem1  34519  isbasisrelowllem2  34520  finxpsuclem  34561  wl-lem-exsb  34684  wl-mo3t  34694  wl-ax11-lem1  34699  matunitlindf  34772  poimirlem6  34780  poimirlem7  34781  poimirlem16  34790  poimirlem19  34793  poimirlem22  34796  poimirlem23  34797  poimirlem24  34798  cnambfre  34822  itg2addnc  34828  brabg2  34874  istotbnd3  34932  sstotbnd2  34935  sstotbnd  34936  sstotbnd3  34937  ssbnd  34949  ismtybnd  34968  reheibor  35000  grpoeqdivid  35042  grpokerinj  35054  rngosn3  35085  rngoueqz  35101  1idl  35187  0rngo  35188  divrngidl  35189  igenval2  35227  ispridlc  35231  isdmn3  35235  relcnveq3  35461  iss2  35484  elrelscnveq3  35613  funALTVeq  35815  disjeq  35849  prtlem10  35883  prter2  35899  dral1-o  35922  lshpinN  36007  lsatcveq0  36050  lsatcv0eq  36065  lsatcv1  36066  islshpcv  36071  lkr0f  36112  lkrshp4  36126  lshpkrlem1  36128  lshpset2N  36137  lfl1dim  36139  lfl1dim2N  36140  lub0N  36207  glb0N  36211  oplecon3b  36218  cmtcomN  36267  cmtbr3N  36272  cmtbr4N  36273  cvrnbtwn2  36293  cvrnbtwn3  36294  cvrcon3b  36295  cvrnbtwn4  36297  cvrcmp  36301  atcvreq0  36332  atnle  36335  atlatle  36338  cvlexchb1  36348  cvlcvr1  36357  hlrelat2  36421  exatleN  36422  cvrval3  36431  cvrval4N  36432  cvrexch  36438  atcvr0eq  36444  lnnat  36445  atcvrj0  36446  atcvrj2b  36450  atltcvr  36453  atbtwn  36464  ps-1  36495  3at  36508  islln2a  36535  llncmp  36540  islpln2a  36566  lplncmp  36580  islvol2aN  36610  4at  36631  lvolcmp  36635  pmaple  36779  lncmp  36801  paddss  36863  llnexchb2lem  36886  2polcon4bN  36936  ispsubcl2N  36965  lhpat3  37064  lautcvr  37110  ltrnid  37153  trlval2  37181  trlatn0  37190  ltrnideq  37193  trlnidatb  37195  cdlemeg49lebilem  37557  trlord  37587  cdlemg1a  37588  cdlemg1cex  37606  tendoid0  37843  dva1dim  38003  cdlemm10N  38136  diarnN  38147  cdlemn  38230  dihlspsnssN  38350  dihatexv  38356  dochkrshp  38404  dochkrshp4  38407  djhlsmcl  38432  lcfl6  38518  lcfl8  38520  lcfrvalsnN  38559  lcfrlem9  38568  mapdval2N  38648  mapdordlem2  38655  mapd1o  38666  mapd0  38683  mapdheq2biN  38748  fnsnbt  39000  frlmfzowrdb  39023  frlmsnic  39029  prjspreln0  39139  elrfi  39171  diophrw  39236  eldioph2b  39240  diophin  39249  rexrabdioph  39271  rmxycomplete  39394  coprmdvdsb  39462  jm2.19  39470  jm2.26  39479  jm2.27  39485  limsuc2  39521  dgraa0p  39629  rngunsnply  39653  fiuneneq  39677  nndomog  39777  pwelg  39799  nzss  40529  dvconstbi  40546  expgrowth  40547  bcc0  40552  axc11next  40618  pm14.24  40644  sbiota1  40646  sbcim2g  40752  sineq0ALT  41151  pwssfi  41187  mapss2  41348  fsneq  41349  fsneqrn  41354  mapssbi  41356  ssmapsn  41359  rnmptbd2lem  41400  infnsuprnmpt  41402  rnmptbdlem  41407  xralrple2  41502  infxrunb2  41516  xralrple4  41521  xralrple3  41522  xrralrecnnle  41533  xrralrecnnge  41542  reclt0  41543  supxrunb3  41552  supxrleubrnmpt  41559  xrre4  41565  unb2ltle  41569  rexabslelem  41572  suprleubrnmpt  41576  infxrunb3rnmpt  41582  uzub  41585  supminfrnmpt  41599  iccintsng  41679  sqrlearg  41709  uzinico  41716  preimaiocmnf  41717  limcresiooub  41803  limclr  41816  climeldmeq  41826  limsuppnflem  41871  limsupmnflem  41881  limsupmnfuzlem  41887  limsupre3lem  41893  limsupre3uzlem  41896  liminfreuzlem  41963  dvnmul  42108  dvmptfprodlem  42109  ismbl3  42152  ismbl4  42159  fourierdlem50  42322  fourierdlem89  42361  fourierdlem91  42363  dfsalgen2  42505  sge0repnf  42549  sge0lefi  42561  sge0resplit  42569  sge0fodjrnlem  42579  voliunsge0lem  42635  hspdifhsp  42779  isvonmbl  42801  ovnovollem3  42821  vonvolmbl  42824  pimrecltpos  42868  preimaicomnf  42871  pimrecltneg  42882  issmflem  42885  issmfle  42903  issmfgt  42914  smfaddlem1  42920  issmfge  42927  smfresal  42944  smflimmpt  42965  smfinflem  42972  smflimsuplem7  42981  smflimsupmpt  42984  sigarcol  43002  confun  43056  or2expropbi  43150  rexsb  43178  euoreqb  43189  ralbinrald  43202  rlimdmafv  43257  fafv2elrnb  43315  tz6.12c-afv2  43322  dfatbrafv2b  43325  fnbrafv2b  43328  rlimdmafv2  43338  f1oresf1o2  43371  el1fzopredsuc  43406  2ffzoeq  43409  iccpartiun  43441  ichnfb  43472  ich2exprop  43480  sprsymrelfolem2  43502  paireqne  43520  prprelprb  43526  reupr  43531  requad01  43633  requad1  43634  requad2  43635  dfodd6  43649  dfeven4  43650  evensumeven  43719  sbgoldbalt  43793  isomushgr  43838  isomuspgr  43846  isomgrsymb  43849  isassintop  44015  uzlidlring  44098  rngciso  44151  rngcisoALTV  44163  ringciso  44202  ringcisoALTV  44226  domnmsuppn0  44315  lindslininds  44417  snlindsntor  44424  isldepslvec2  44438  affinecomb1  44587  prelrrx2b  44599  rrx2plord2  44607  eenglngeehlnm  44624  rrx2vlinest  44626  line2xlem  44638  line2x  44639  line2y  44640  itsclc0xyqsolb  44655  itsclquadb  44661
  Copyright terms: Public domain W3C validator