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

Theorem impbid 202
Description: Deduce an equivalence from two implications. Deduction associated with impbi 198 and impbii 199. (Contributed by NM, 24-Jan-1993.) Revised to prove it from impbid21d 201. (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 201 . 2 (𝜑 → (𝜑 → (𝜓𝜒)))
43pm2.43i 52 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
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
This theorem is referenced by:  bicom1  211  impbid1  215  impcon4bid  217  pm5.74  259  imbi1d  330  pm5.501  355  2falsed  365  impbida  913  dedlem0b  1031  dedlema  1032  dedlemb  1033  albi  1895  alexbii  1909  equequ1  2107  equequ2  2108  elequ1  2146  elequ2  2153  19.21tOLDOLD  2221  sbequ12  2258  sb56  2297  19.21tOLD  2358  cbv2h  2414  dral1  2465  dral1ALT  2466  ax12b  2482  sbequ  2513  sbft  2516  exsb  2605  eupickb  2676  eupickbi  2677  2eu2  2692  ceqsalt  3368  rspcebdv  3454  ceqex  3472  mob2  3527  reu6  3536  sbciegft  3607  eqsbc3rOLD  3634  csbiebt  3694  sseq1  3767  ssdifsym  4006  reupick  4054  reupick2  4056  uneqdifeq  4201  uneqdifeqOLD  4202  eqoreldifOLD  4370  prnebg  4533  preqsnd  4536  prel12g  4544  disjeq2  4776  disjeq1  4779  disjss3  4803  reusv2lem2  5018  reusv2lem2OLD  5019  reusv2lem3  5020  alxfr  5027  ralxfrd  5028  ralxfrdOLD  5029  ralxfrd2  5033  copsexg  5104  euotd  5123  poeq2  5191  sotric  5213  sotrieq  5214  freq2  5237  seeq1  5238  seeq2  5239  iss  5605  tz7.7  5910  ordtri1  5917  ordtri3OLD  5921  ordelinel  5986  ordelinelOLD  5987  iotaval  6023  funeq  6069  funssres  6091  f0dom0  6250  tz6.12c  6375  fnbrfvb  6398  ssimaex  6426  fvimacnv  6496  elpreima  6501  eldmrexrnb  6530  fsn  6566  fnsnb  6597  fmptsng  6599  fmptsnd  6600  tpres  6631  fconst2g  6633  fconst5  6636  elunirn  6673  f1ocnvfvb  6699  foeqcnvco  6719  f1eqcocnv  6720  fliftfun  6726  soisores  6741  isofr  6756  isose  6757  isopo  6760  isoso  6762  f1oiso2  6766  eusvobj2  6807  oprabid  6841  f1opw2  7054  oneqmin  7171  ordsuc  7180  ordelsuc  7186  ordsucelsuc  7188  ordunisuc2  7210  limsuc  7215  f1ovv  7303  op1steq  7378  fvn0elsuppb  7481  extmptsuppeq  7488  rntpos  7535  smoiso2  7636  seqomlem2  7716  oaord  7798  oawordex  7808  oaordex  7809  omord2  7818  om00  7826  oeord  7839  nnaord  7870  nnmord  7883  nnawordex  7888  nnaordex  7889  erexb  7938  swoord1  7944  swoord2  7945  iiner  7988  eceqoveq  8021  ralxpmap  8075  omxpenlem  8228  domtriord  8273  mapxpen  8293  mapunen  8296  ssenen  8301  nneneq  8310  onomeneq  8317  nndomo  8321  en1eqsnbi  8358  fodomfib  8407  f1opwfi  8437  fsuppunbi  8463  elfiun  8503  suplub2  8534  ordiso2  8587  ordiso  8588  oieu  8611  brwdom2  8645  brwdom3  8654  cantnflem1  8761  cardidm  8995  carddom2  9013  pm54.43  9036  pr2ne  9038  acnen  9086  acnen2  9088  alephord  9108  alephinit  9128  dfac5  9161  infdif2  9244  fictb  9279  coflim  9295  fincssdom  9357  fin23lem25  9358  isf32lem9  9395  isf34lem4  9411  fin1a2lem11  9444  axdc3lem2  9485  ficard  9599  fpwwe2lem12  9675  fpwwe2  9677  indpi  9941  nqereq  9969  1idpr  10063  ltapr  10079  leltne  10339  ltlen  10350  ltadd2  10353  addlsub  10659  addid0  10662  ltord1  10766  mul0or  10879  ltmul1  11085  mulge0b  11105  lt2msq  11120  negfi  11183  nnsub  11271  nn0sub  11555  zrevaddcl  11634  zltp1le  11639  zdiv  11659  nneo  11673  zeo2  11676  zmax  11998  zbtwnre  11999  qrevaddcl  12023  xrlttri  12185  xrleltne  12191  xralrple  12249  xltneg  12261  xleadd1  12298  xlemul1  12333  supxrunb1  12362  supxrunb2  12363  ioo0  12413  iccid  12433  ico0  12434  ioc0  12435  icc0  12436  difreicc  12517  iccsplit  12518  zltaddlt1le  12537  0fz1  12574  uzsplit  12625  fzm1  12633  fzrevral  12638  ssfzo12bi  12777  elfznelfzob  12788  flge  12820  modid2  12911  modmuladd  12926  ssnn0fi  12998  seqf1olem1  13054  hashen  13349  hashdom  13380  hash2exprb  13465  pr2pwpr  13473  hashtpg  13479  len0nnbi  13547  reuccats1  13700  ccats1swrdeqbi  13718  repsdf2  13745  scshwfzeqfzo  13792  relexpindlem  14022  shftlem  14027  shftuz  14028  abslt  14273  absle  14274  rexico  14312  cau3lem  14313  rlim2lt  14447  rlim3  14448  o1lo1  14487  rlimdm  14501  climshft  14526  o1dif  14579  isercolllem2  14615  isercoll  14617  zsum  14668  fsum  14670  fsum00  14749  incexclem  14787  zprod  14886  fprod  14890  dvdsval2  15205  moddvds  15213  negdvdsb  15220  dvdsnegb  15221  dvdscmulr  15232  dvdsmulcr  15233  dvdssub2  15245  dvdsaddre2b  15251  fzo0dvdseq  15267  mod2eq1n2dvds  15293  ltoddhalfle  15307  sumodd  15333  bitsf1ocnv  15388  sadcaddlem  15401  bitsuz  15418  dvdsgcdb  15484  gcdzeq  15493  dvdssqlem  15501  lcmeq0  15535  lcmdvdsb  15548  lcmfeq0b  15565  lcmf  15568  lcmfdvdsb  15578  coprmgcdb  15584  cncongr  15605  isprm2lem  15616  dvdsprime  15622  dvdsprm  15637  isprm7  15642  coprm  15645  euclemma  15647  rpexp  15654  prmdiveq  15713  hashgcdlem  15715  odzdvds  15722  pythagtrip  15761  pc2dvds  15805  pcprmpw2  15808  pcprmpw  15809  vdwapun  15900  ramtcl2  15937  firest  16315  mrieqv2d  16521  isacs2  16535  isssc  16701  setciso  16962  posasymb  17173  pleval2  17186  pltval3  17188  lublecllem  17209  joinle  17235  meetle  17249  lubun  17344  clatleglb  17347  latdisd  17411  letsr  17448  intopsn  17474  gsumval2a  17500  frmdss2  17621  isgrpid2  17679  isgrpinv  17693  symg1bas  18036  oddvdsnn0  18183  oddvds  18186  odeq  18189  odeq1  18197  gexdvds  18219  pgpfi  18240  pgpssslw  18249  fislw  18260  sylow3lem2  18263  lsmelvalm  18286  lsmlub  18298  lsmss1b  18300  lsmss2b  18302  efgs1b  18369  cyggenod  18506  cyggexb  18520  dprdfeq0  18641  ringinvnz1ne0  18812  ringinvnzdiv  18813  unitmulclb  18885  dvreq1  18913  f1rhm0to0  18962  f1rhm0to0ALT  18963  drngmul0or  18990  isabvd  19042  issrngd  19083  lssats2  19222  lspsneq0  19234  lsmelval2  19307  lvecvs0or  19330  lspsneq  19344  lspsneu  19345  lidl1el  19440  lidldvgen  19477  isnzr2  19485  0ringnnzr  19491  0ring01eqbi  19495  rrgeq0  19512  domneq0  19519  ply1coe1eq  19890  cply1coe0bi  19892  znunit  20134  psgndif  20170  ipeq0  20205  ocvsscon  20241  pjdm2  20277  obselocv  20294  islinds4  20396  mat1dimelbas  20499  cramer  20719  toponcomb  20955  tgss3  21012  clsval2  21076  isopn3  21092  elcls3  21109  opncldf1  21110  neiint  21130  neips  21139  opnneissb  21140  opnssneib  21141  opnnei  21146  tpnei  21147  opnneiid  21152  restcld  21198  restopnb  21201  tgcn  21278  tgcnp  21279  subbascn  21280  iscnp4  21289  cnpnei  21290  cncls2  21299  cncls  21300  cnntr  21301  lmss  21324  hausnei2  21379  lpcls  21390  ordtt1  21405  cmpsub  21425  tgcmp  21426  1stcelcls  21486  locfincmp  21551  kgencn2  21582  ptpjpre1  21596  upxp  21648  txcn  21651  txlm  21673  tgqtop  21737  kqfvima  21755  isr0  21762  regr1lem2  21765  hmeoopn  21791  hmeocld  21792  ptuncnv  21832  fbunfip  21894  fgss2  21899  ufilb  21931  ufprim  21934  trufil  21935  cfinufil  21953  ufildr  21956  elfm2  21973  elfm3  21975  rnelfm  21978  fmfnfmlem4  21982  fmco  21986  flimtopon  21995  flimopn  22000  fbflim2  22002  flimrest  22008  flffbas  22020  cnpflf  22026  fclstopon  22037  fclsnei  22044  fclsbas  22046  fclsfnflim  22052  fclscmp  22055  ufilcmp  22057  isfcf  22059  fcfnei  22060  cnpfcf  22066  alexsubb  22071  alexsubALT  22076  cldsubg  22135  tgphaus  22141  tgpt0  22143  tsmsgsum  22163  tsmsres  22168  xbln0  22440  blssexps  22452  blssex  22453  isxms2  22474  prdsbl  22517  neibl  22527  metss  22534  met2ndc  22549  metrest  22550  metcnp3  22566  tngngp3  22681  nmoeq0  22761  xrsxmet  22833  reconn  22852  iccpnfcnv  22964  fgcfil  23289  iscau4  23297  cfilres  23314  iunmbl2  23545  ismbf3d  23640  mbfaddlem  23646  i1faddlem  23679  i1fmullem  23680  ellimc3  23862  tdeglem4  24039  deg1nn0clb  24069  deg1lt0  24070  dvdsq1p  24139  plypf1  24187  0dgrb  24221  plymul0or  24255  ulmshft  24363  ulmcaulem  24367  ulmcau  24368  cosord  24498  eff1olem  24514  lognegb  24556  eflogeq  24568  logdivlt  24587  efopn  24624  cxpeq0  24644  cxpeq  24718  angpieqvd  24778  dcubic  24793  asinsinb  24844  acoscosb  24845  atantanb  24871  rlimcnp  24912  isppw  25060  isppw2  25061  vmappw  25062  isnsqf  25081  ppieq0  25122  fsumdvdsdiag  25130  dvdsppwf1o  25132  fsumfldivdiag  25136  chpeq0  25153  chteq0  25154  dchrptlem1  25209  lgsdir2lem4  25273  lgsne0  25280  lgsqr  25296  lgsdchrval  25299  gausslemma2dlem1a  25310  lgsquadlem1  25325  m1lgs  25333  iscgrglt  25629  brbtwn  25999  brcgr  26000  brbtwn2  26005  axcontlem7  26070  uhgr0vb  26187  edglnl  26258  ausgrusgrb  26280  ushgredgedg  26341  ushgredgedgloop  26343  usgr0vb  26349  usgr1v  26368  nbupgr  26460  nbumgrvtx  26462  nbuhgr2vtx1edgb  26468  edgusgrnbfin  26494  nb3grprlem1  26501  uvtxnbvtxm1  26532  cusgrfilem2  26583  uhgr0edg0rgrb  26701  cusgrm1rusgr  26709  spthonepeq  26879  usgr2pth  26891  wlkiswwlks  27006  wlkiswwlkupgr  27008  wlklnwwlkn  27014  wlklnwwlknupgr  27016  wwlksnextbi  27033  wwlksnredwwlkn0  27035  wwlksnextwrd  27036  wwlksnextprop  27051  wwlksnwwlksnonOLD  27056  elwwlks2ons3OLD  27097  umgrwwlks2on  27099  elwspths2on  27102  usgr2wspthons3  27107  elwwlks2  27109  elwspths2spth  27110  clwlkclwwlklem3  27145  loopclwwlkn1b  27192  clwwlknon1sn  27269  clwwlknonwwlknonb  27275  clwwlknonwwlknonbOLD  27276  clwwlknunOLD  27286  umgr3v3e3cycl  27357  eupth2lem3lem4  27404  frgr0v  27436  frgr3vlem2  27449  2clwwlk2clwwlk  27528  wlkl0  27549  grpoinvf  27716  nvmul0or  27835  nvz  27854  diporthcom  27901  ubthlem3  28058  hvmul0or  28212  his6  28286  hial0  28289  hial02  28290  orthcom  28295  normgt0  28314  ocin  28485  occon3  28486  shsel3  28504  shlub  28603  chssoc  28685  h1de2bi  28743  spansncol  28757  elspansn4  28762  spansnss2  28764  sumspansn  28838  lnopcnbd  29225  lnfncnbd  29246  riesz1  29254  elpjrn  29379  cvcon3  29473  dmdmd  29489  dmdbr3  29494  dmdbr4  29495  dmdbr5  29497  mdslmd1i  29518  atcveq0  29537  chcv1  29544  atssma  29567  atcv0eq  29568  atcv1  29569  bian1d  29636  disjeq1f  29715  br8d  29750  fpwrelmap  29838  xaddeq0  29848  eliccelico  29869  elicoelioo  29870  isarchiofld  30147  unitdivcld  30277  xrge0iifcnv  30309  lmxrge0  30328  indf1ofs  30418  eulerpartlemgh  30770  dstfrvunirn  30866  cvmliftmolem2  31592  cvmlift2lem12  31624  mthmb  31806  climuzcnv  31893  br8  31974  br6  31975  br4  31976  funbreq  31996  fprb  31997  axext4dist  32032  nodenselem8  32168  dfrdg4  32385  cgrcom  32424  cgrcoml  32430  cgrdegen  32438  btwncom  32448  brsegle  32542  brsegle2  32543  colinbtwnle  32552  btwnoutside  32559  broutsideof3  32560  outsidele  32566  lineunray  32581  lineelsb2  32582  elhf2  32609  elicc3  32638  nn0prpwlem  32644  opnbnd  32647  cldbnd  32648  opnregcld  32652  cldregopn  32653  fnessref  32679  refssfne  32680  neibastop2  32683  fnemeet2  32689  fnejoin2  32691  fgmin  32692  ontgval  32757  ordtop  32762  ordcmp  32773  nndivsub  32783  bj-ssbbi  32950  bj-ssbft  32970  bj-cbv2hv  33059  bj-dral1v  33076  bj-sbftv  33091  bj-equsal1t  33137  bj-19.21t  33145  bj-ceqsalt0  33195  bj-ceqsalt1  33196  bj-xpnzexb  33272  bj-finsumval0  33476  bj-ldiv  33484  bj-bary1  33491  dfgcd3  33499  isbasisrelowllem1  33532  isbasisrelowllem2  33533  finxpsuclem  33563  wl-lem-exsb  33679  wl-mo3t  33689  wl-ax11-lem1  33693  wl-clelv2-just  33710  matunitlindf  33738  poimirlem6  33746  poimirlem7  33747  poimirlem16  33756  poimirlem19  33759  poimirlem22  33762  poimirlem23  33763  poimirlem24  33764  cnambfre  33789  itg2addnc  33795  brabg2  33841  istotbnd3  33901  sstotbnd2  33904  sstotbnd  33905  sstotbnd3  33906  ssbnd  33918  ismtybnd  33937  reheibor  33969  grpoeqdivid  34011  grpokerinj  34023  rngosn3  34054  rngoueqz  34070  1idl  34156  0rngo  34157  divrngidl  34158  igenval2  34196  ispridlc  34200  isdmn3  34204  relcnveq3  34434  iss2  34453  elrelscnveq3  34582  prtlem10  34672  prter2  34688  dral1-o  34711  lshpinN  34797  lsatcveq0  34840  lsatcv0eq  34855  lsatcv1  34856  islshpcv  34861  lkr0f  34902  lkrshp4  34916  lshpkrlem1  34918  lshpset2N  34927  lfl1dim  34929  lfl1dim2N  34930  lub0N  34997  glb0N  35001  oplecon3b  35008  cmtcomN  35057  cmtbr3N  35062  cmtbr4N  35063  cvrnbtwn2  35083  cvrnbtwn3  35084  cvrcon3b  35085  cvrnbtwn4  35087  cvrcmp  35091  atcvreq0  35122  atnle  35125  atlatle  35128  cvlexchb1  35138  cvlcvr1  35147  hlrelat2  35210  exatleN  35211  cvrval3  35220  cvrval4N  35221  cvrexch  35227  atcvr0eq  35233  lnnat  35234  atcvrj0  35235  atcvrj2b  35239  atltcvr  35242  atbtwn  35253  ps-1  35284  3at  35297  islln2a  35324  llncmp  35329  islpln2a  35355  lplncmp  35369  islvol2aN  35399  4at  35420  lvolcmp  35424  pmaple  35568  lncmp  35590  paddss  35652  llnexchb2lem  35675  2polcon4bN  35725  ispsubcl2N  35754  lhpat3  35853  lautcvr  35899  ltrnid  35942  trlval2  35971  trlatn0  35980  ltrnideq  35983  trlnidatb  35985  cdlemeg49lebilem  36347  trlord  36377  cdlemg1a  36378  cdlemg1cex  36396  tendoid0  36633  dva1dim  36793  cdlemm10N  36927  diarnN  36938  cdlemn  37021  dihlspsnssN  37141  dihatexv  37147  dochkrshp  37195  dochkrshp4  37198  djhlsmcl  37223  lcfl6  37309  lcfl8  37311  lcfrvalsnN  37350  lcfrlem9  37359  mapdval2N  37439  mapdordlem2  37446  mapd1o  37457  mapd0  37474  mapdheq2biN  37539  elrfi  37777  diophrw  37842  eldioph2b  37846  diophin  37856  rexrabdioph  37878  rmxycomplete  38002  coprmdvdsb  38072  jm2.19  38080  jm2.26  38089  jm2.27  38095  limsuc2  38131  dgraa0p  38239  rngunsnply  38263  fiuneneq  38295  pwelg  38385  nzss  39036  dvconstbi  39053  expgrowth  39054  bcc0  39059  axc11next  39127  pm14.24  39153  sbiota1  39155  sbcim2g  39268  sineq0ALT  39690  pwssfi  39728  elixpconstg  39783  mapsnd  39905  mapss2  39914  fsneq  39915  fsneqrn  39920  mapssbi  39922  ssmapsn  39925  rnmptbd2lem  39980  infnsuprnmpt  39982  rnmptbdlem  39987  xralrple2  40086  infxrunb2  40100  xralrple4  40105  xralrple3  40106  xrralrecnnle  40118  xrralrecnnge  40129  reclt0  40130  supxrunb3  40139  supxrleubrnmpt  40148  xrre4  40154  unb2ltle  40158  rexabslelem  40161  suprleubrnmpt  40165  infxrunb3rnmpt  40171  uzub  40174  supminfrnmpt  40188  iccintsng  40270  sqrlearg  40301  uzinico  40308  preimaiocmnf  40309  limcresiooub  40395  limclr  40408  climeldmeq  40418  limsuppnflem  40463  limsupmnflem  40473  limsupmnfuzlem  40479  limsupre3lem  40485  limsupre3uzlem  40488  liminfreuzlem  40555  dvnmul  40679  dvmptfprodlem  40680  ismbl3  40724  ismbl4  40731  fourierdlem50  40894  fourierdlem89  40933  fourierdlem91  40935  dfsalgen2  41080  sge0repnf  41124  sge0lefi  41136  sge0resplit  41144  sge0fodjrnlem  41154  voliunsge0lem  41210  hspdifhsp  41354  isvonmbl  41376  ovnovollem3  41396  vonvolmbl  41399  preimagelt  41436  preimalegt  41437  pimrecltpos  41443  preimaicomnf  41446  pimrecltneg  41457  issmflem  41460  issmfle  41478  issmfgt  41489  smfaddlem1  41495  issmfge  41502  smfresal  41519  smflimmpt  41540  smfinflem  41547  smflimsuplem7  41556  smflimsupmpt  41559  sigarcol  41577  confun  41630  rexsb  41692  2reu2  41711  ralbinrald  41723  rlimdmafv  41781  el1fzopredsuc  41863  2ffzoeq  41866  iccpartiun  41898  ccats1pfxeqbi  41959  reuccatpfxs1  41962  dfodd6  42078  dfeven4  42079  evensumeven  42144  sbgoldbalt  42197  sprsymrelfolem2  42271  isassintop  42374  uzlidlring  42457  rngciso  42510  rngcisoALTV  42522  ringciso  42561  ringcisoALTV  42585  domnmsuppn0  42678  lindslininds  42781  snlindsntor  42788  isldepslvec2  42802
  Copyright terms: Public domain W3C validator