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

Theorem impbid 200
Description: Deduce an equivalence from two implications. Deduction associated with impbi 196 and impbii 197. (Contributed by NM, 24-Jan-1993.) Revised to prove it from impbid21d 199. (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 199 . 2 (𝜑 → (𝜑 → (𝜓𝜒)))
43pm2.43i 49 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194
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
This theorem is referenced by:  bicom1  209  impbid1  213  impcon4bid  215  pm5.74  257  imbi1d  329  pm5.501  354  2falsed  364  impbida  872  dedlem0b  991  dedlema  992  dedlemb  993  albi  1735  alexbii  1749  exbiOLD  1762  equequ1  1938  equequ2  1939  elequ1  1983  elequ2  1990  19.21t  2060  sbequ12  2096  sb56  2135  19.21tOLD  2200  cbv2h  2256  dral1  2312  dral1ALT  2313  ax12b  2332  sbequ  2363  sbft  2366  exsb  2455  eupickb  2525  eupickbi  2526  2eu2  2541  eleq2dOLD  2673  ceqsalt  3200  ceqex  3302  mob2  3352  reu6  3361  sbciegft  3432  eqsbc3rOLD  3459  csbiebt  3518  sseq1  3588  reupick  3869  reupick2  3871  uneqdifeq  4008  uneqdifeqOLD  4009  eqoreldifOLD  4172  prnebg  4324  disjeq2  4551  disjeq1  4554  disjxiunOLD  4574  disjss3  4576  reusv2lem2  4790  reusv2lem2OLD  4791  reusv2lem3  4792  alxfr  4799  ralxfrd  4800  ralxfrdOLD  4801  ralxfrd2  4805  copsexg  4876  euotd  4891  poeq2  4953  sotric  4975  sotrieq  4976  freq2  4999  seeq1  5000  seeq2  5001  iss  5354  tz7.7  5652  ordtri1  5659  ordtri3OLD  5663  ordelinel  5728  ordelinelOLD  5729  iotaval  5765  funeq  5809  funssres  5830  f0dom0  5987  tz6.12c  6108  fnbrfvb  6131  ssimaex  6158  fvimacnv  6225  elpreima  6230  eldmrexrnb  6259  fsn  6293  fnsnb  6315  fmptsng  6317  fmptsnd  6318  tpres  6349  fconst2g  6351  fconst5  6354  elunirn  6391  f1ocnvfvb  6413  foeqcnvco  6433  f1eqcocnv  6434  fliftfun  6440  soisores  6455  isofr  6470  isose  6471  isopo  6474  isoso  6476  f1oiso2  6480  eusvobj2  6520  oprabid  6554  f1opw2  6763  oneqmin  6874  ordsuc  6883  ordelsuc  6889  ordsucelsuc  6891  ordunisuc2  6913  limsuc  6918  f1ovv  7007  op1steq  7078  fvn0elsuppb  7176  extmptsuppeq  7183  rntpos  7229  smoiso2  7330  seqomlem2  7410  oaord  7491  oawordex  7501  oaordex  7502  omord2  7511  om00  7519  oeord  7532  nnaord  7563  nnmord  7576  nnawordex  7581  nnaordex  7582  erexb  7631  swoord1  7637  swoord2  7638  iiner  7683  eceqoveq  7717  ralxpmap  7770  omxpenlem  7923  domtriord  7968  mapxpen  7988  mapunen  7991  ssenen  7996  nneneq  8005  onomeneq  8012  nndomo  8016  en1eqsnbi  8053  fodomfib  8102  f1opwfi  8130  fsuppunbi  8156  elfiun  8196  suplub2  8227  ordiso2  8280  ordiso  8281  oieu  8304  brwdom2  8338  brwdom3  8347  cantnflem1  8446  cardidm  8645  carddom2  8663  pm54.43  8686  pr2ne  8688  acnen  8736  acnen2  8738  alephord  8758  alephinit  8778  dfac5  8811  infdif2  8892  fictb  8927  coflim  8943  fincssdom  9005  fin23lem25  9006  isf32lem9  9043  isf34lem4  9059  fin1a2lem11  9092  axdc3lem2  9133  ficard  9243  fpwwe2lem12  9319  fpwwe2  9321  indpi  9585  nqereq  9613  1idpr  9707  ltapr  9723  leltne  9978  ltlen  9989  ltadd2  9992  addlsub  10298  addid0  10301  ltord1  10403  mul0or  10516  ltmul1  10722  mulge0b  10742  lt2msq  10757  negfi  10820  nnsub  10906  nn0sub  11190  zrevaddcl  11255  zltp1le  11260  zdiv  11279  nneo  11293  zeo2  11296  zmax  11617  zbtwnre  11618  qrevaddcl  11642  xrlttri  11807  xrleltne  11813  xralrple  11869  xltneg  11881  xleadd1  11914  xlemul1  11949  supxrunb1  11977  supxrunb2  11978  ioo0  12027  iccid  12047  ico0  12048  ioc0  12049  icc0  12050  difreicc  12131  iccsplit  12132  zltaddlt1le  12151  0fz1  12187  uzsplit  12236  fzm1  12244  fzrevral  12249  ssfzo12bi  12384  elfznelfzob  12395  flge  12423  modid2  12514  modmuladd  12529  ssnn0fi  12601  seqf1olem1  12657  hashen  12949  hashdom  12981  hashle00  13001  hash2exprb  13062  pr2pwpr  13066  hashtpg  13071  reuccats1  13278  ccats1swrdeqbi  13295  repsdf2  13322  scshwfzeqfzo  13369  relexpindlem  13597  shftlem  13602  shftuz  13603  abslt  13848  absle  13849  rexico  13887  cau3lem  13888  rlim2lt  14022  rlim3  14023  o1lo1  14062  rlimdm  14076  climshft  14101  o1dif  14154  isercolllem2  14190  isercoll  14192  zsum  14242  fsum  14244  fsum00  14317  incexclem  14353  zprod  14452  fprod  14456  dvdsval2  14770  moddvds  14775  negdvdsb  14782  dvdsnegb  14783  dvdscmulr  14794  dvdsmulcr  14795  dvdssub2  14807  dvdsaddre2b  14813  fzo0dvdseq  14829  mod2eq1n2dvds  14855  ltoddhalfle  14869  sumodd  14895  bitsf1ocnv  14950  sadcaddlem  14963  bitsuz  14980  dvdsgcdb  15046  gcdzeq  15055  dvdssqlem  15063  lcmeq0  15097  lcmdvdsb  15110  lcmfeq0b  15127  lcmf  15130  lcmfdvdsb  15140  coprmgcdb  15146  cncongr  15167  isprm2lem  15178  dvdsprime  15184  dvdsprm  15199  isprm7  15204  coprm  15207  euclemma  15209  rpexp  15216  prmdiveq  15275  hashgcdlem  15277  odzdvds  15284  pythagtrip  15323  pc2dvds  15367  pcprmpw2  15370  pcprmpw  15371  vdwapun  15462  ramtcl2  15499  firest  15862  mrieqv2d  16068  isacs2  16083  isssc  16249  setciso  16510  posasymb  16721  pleval2  16734  pltval3  16736  lublecllem  16757  joinle  16783  meetle  16797  lubun  16892  clatleglb  16895  latdisd  16959  letsr  16996  intopsn  17022  gsumval2a  17048  frmdss2  17169  isgrpid2  17227  isgrpinv  17241  symg1bas  17585  oddvdsnn0  17732  oddvds  17735  odeq  17738  odeq1  17746  gexdvds  17768  pgpfi  17789  pgpssslw  17798  fislw  17809  sylow3lem2  17812  lsmelvalm  17835  lsmlub  17847  lsmss1b  17849  lsmss2b  17851  efgs1b  17918  cyggenod  18055  cyggexb  18069  dprdfeq0  18190  ringinvnz1ne0  18361  ringinvnzdiv  18362  unitmulclb  18434  dvreq1  18462  f1rhm0to0  18509  f1rhm0to0ALT  18510  drngmul0or  18537  isabvd  18589  issrngd  18630  lssats2  18767  lspsneq0  18779  lsmelval2  18852  lvecvs0or  18875  lspsneq  18889  lspsneu  18890  lidl1el  18985  lidldvgen  19022  isnzr2  19030  0ringnnzr  19036  0ring01eqbi  19040  rrgeq0  19057  domneq0  19064  ply1coe1eq  19435  cply1coe0bi  19437  znunit  19676  psgndif  19712  ipeq0  19747  ocvsscon  19780  pjdm2  19816  obselocv  19833  islinds4  19935  mat1dimelbas  20038  cramer  20258  tgss3  20543  clsval2  20606  isopn3  20622  elcls3  20639  opncldf1  20640  neiint  20660  neips  20669  opnneissb  20670  opnssneib  20671  opnnei  20676  tpnei  20677  opnneiid  20682  restcld  20728  restopnb  20731  tgcn  20808  tgcnp  20809  subbascn  20810  iscnp4  20819  cnpnei  20820  cncls2  20829  cncls  20830  cnntr  20831  lmss  20854  hausnei2  20909  lpcls  20920  ordtt1  20935  cmpsub  20955  tgcmp  20956  1stcelcls  21016  locfincmp  21081  kgencn2  21112  ptpjpre1  21126  upxp  21178  txcn  21181  txlm  21203  tgqtop  21267  kqfvima  21285  isr0  21292  regr1lem2  21295  hmeoopn  21321  hmeocld  21322  ptuncnv  21362  fbunfip  21425  fgss2  21430  ufilb  21462  ufprim  21465  trufil  21466  cfinufil  21484  ufildr  21487  elfm2  21504  elfm3  21506  rnelfm  21509  fmfnfmlem4  21513  fmco  21517  flimtopon  21526  flimopn  21531  fbflim2  21533  flimrest  21539  flffbas  21551  cnpflf  21557  fclstopon  21568  fclsnei  21575  fclsbas  21577  fclsfnflim  21583  fclscmp  21586  ufilcmp  21588  isfcf  21590  fcfnei  21591  cnpfcf  21597  alexsubb  21602  alexsubALT  21607  cldsubg  21666  tgphaus  21672  tgpt0  21674  tsmsgsum  21694  tsmsres  21699  xbln0  21970  blssexps  21982  blssex  21983  isxms2  22004  prdsbl  22047  neibl  22057  metss  22064  met2ndc  22079  metrest  22080  metcnp3  22096  nmoeq0  22282  xrsxmet  22352  reconn  22371  iccpnfcnv  22482  fgcfil  22795  iscau4  22803  cfilres  22820  iunmbl2  23049  ismbf3d  23144  mbfaddlem  23150  i1faddlem  23183  i1fmullem  23184  ellimc3  23366  tdeglem4  23541  deg1nn0clb  23571  deg1lt0  23572  dvdsq1p  23641  plypf1  23689  0dgrb  23723  plymul0or  23757  ulmshft  23865  ulmcaulem  23869  ulmcau  23870  cosord  23999  eff1olem  24015  lognegb  24057  eflogeq  24069  logdivlt  24088  efopn  24121  cxpeq0  24141  cxpeq  24215  angpieqvd  24275  dcubic  24290  asinsinb  24341  acoscosb  24342  atantanb  24368  rlimcnp  24409  isppw  24557  isppw2  24558  vmappw  24559  isnsqf  24578  ppieq0  24619  fsumdvdsdiag  24627  dvdsppwf1o  24629  fsumfldivdiag  24633  chpeq0  24650  chteq0  24651  dchrptlem1  24706  lgsdir2lem4  24770  lgsne0  24777  lgsqr  24793  lgsdchrval  24796  gausslemma2dlem1a  24807  lgsquadlem1  24822  m1lgs  24830  iscgrglt  25127  brbtwn  25497  brcgr  25498  brbtwn2  25503  axcontlem7  25568  ausisusgra  25650  nbgraf1olem5  25740  edgusgranbfin  25745  nb3graprlem1  25746  cusgrarn  25754  nbcusgra  25758  cusgrafilem2  25774  uvtxnbgra  25787  uvtxnb  25791  spthonepeq  25883  3v3e3cycl  25959  wlkiswwlk  25992  wlklniswwlkn  25995  wwlknextbi  26019  wwlknredwwlkn0  26021  wwlkextwrd  26022  wwlkextprop  26038  0clwlk  26059  clwlkisclwwlklem0  26082  el2wlkonot  26162  el2spthonot  26163  el2wlkonotot0  26165  el2wlksotot  26175  usg2wlkonot  26176  usg2spthonot  26181  usg2spthonot0  26182  nbhashuvtx  26209  uvtxhashnb  26210  0eusgraiff0rgra  26232  cusgraiffrusgra  26233  eupath2lem3  26272  frgra3vlem2  26294  frgrancvvdeqlem3  26325  grpoinvf  26536  nvmul0or  26677  nvz  26702  diporthcom  26759  ubthlem3  26918  hvmul0or  27072  his6  27146  hial0  27149  hial02  27150  orthcom  27155  normgt0  27174  ocin  27345  occon3  27346  shsel3  27364  shlub  27463  chssoc  27545  h1de2bi  27603  spansncol  27617  elspansn4  27622  spansnss2  27624  sumspansn  27698  lnopcnbd  28085  lnfncnbd  28106  riesz1  28114  elpjrn  28239  cvcon3  28333  dmdmd  28349  dmdbr3  28354  dmdbr4  28355  dmdbr5  28357  mdslmd1i  28378  atcveq0  28397  chcv1  28404  atssma  28427  atcv0eq  28428  atcv1  28429  bian1d  28496  disjeq1f  28575  br8d  28608  fpwrelmap  28702  xaddeq0  28713  eliccelico  28735  elicoelioo  28736  isarchiofld  28954  unitdivcld  29081  xrge0iifcnv  29113  lmxrge0  29132  indf1ofs  29221  eulerpartlemgh  29573  dstfrvunirn  29669  bnj145OLD  29855  cvmliftmolem2  30324  cvmlift2lem12  30356  mthmb  30538  climuzcnv  30625  br8  30705  br6  30706  br4  30707  funbreq  30720  fprb  30722  axext4dist  30756  nodenselem8  30893  dfrdg4  31034  cgrcom  31073  cgrcoml  31079  cgrdegen  31087  btwncom  31097  brsegle  31191  brsegle2  31192  colinbtwnle  31201  btwnoutside  31208  broutsideof3  31209  outsidele  31215  lineunray  31230  lineelsb2  31231  elhf2  31258  elicc3  31287  nn0prpwlem  31293  opnbnd  31296  cldbnd  31297  opnregcld  31301  cldregopn  31302  fnessref  31328  refssfne  31329  neibastop2  31332  fnemeet2  31338  fnejoin2  31340  fgmin  31341  ontgval  31406  ordtop  31411  ordcmp  31422  nndivsub  31432  bj-ssbbi  31617  bj-ssbft  31637  bj-cbv2hv  31724  bj-dral1v  31742  bj-sbftv  31757  bj-equsal1t  31803  bj-19.21t  31811  bj-ceqsalt0  31863  bj-ceqsalt1  31864  bj-xpnzexb  31937  bj-xnex  32041  bj-finsumval0  32120  bj-ldiv  32128  bj-bary1  32135  isbasisrelowllem1  32175  isbasisrelowllem2  32176  finxpsuclem  32206  wl-lem-exsb  32323  wl-mo3t  32333  wl-ax11-lem1  32337  matunitlindf  32373  poimirlem6  32381  poimirlem7  32382  poimirlem16  32391  poimirlem19  32394  poimirlem22  32397  poimirlem23  32398  poimirlem24  32399  cnambfre  32424  itg2addnc  32430  brabg2  32476  istotbnd3  32536  sstotbnd2  32539  sstotbnd  32540  sstotbnd3  32541  ssbnd  32553  ismtybnd  32572  reheibor  32604  grpoeqdivid  32646  grpokerinj  32658  rngosn3  32689  rngoueqz  32705  1idl  32791  0rngo  32792  divrngidl  32793  igenval2  32831  ispridlc  32835  isdmn3  32839  prtlem10  32964  prter2  32980  dral1-o  33003  lshpinN  33090  lsatcveq0  33133  lsatcv0eq  33148  lsatcv1  33149  islshpcv  33154  lkr0f  33195  lkrshp4  33209  lshpkrlem1  33211  lshpset2N  33220  lfl1dim  33222  lfl1dim2N  33223  lub0N  33290  glb0N  33294  oplecon3b  33301  cmtcomN  33350  cmtbr3N  33355  cmtbr4N  33356  cvrnbtwn2  33376  cvrnbtwn3  33377  cvrcon3b  33378  cvrnbtwn4  33380  cvrcmp  33384  atcvreq0  33415  atnle  33418  atlatle  33421  cvlexchb1  33431  cvlcvr1  33440  hlrelat2  33503  exatleN  33504  cvrval3  33513  cvrval4N  33514  cvrexch  33520  atcvr0eq  33526  lnnat  33527  atcvrj0  33528  atcvrj2b  33532  atltcvr  33535  atbtwn  33546  ps-1  33577  3at  33590  islln2a  33617  llncmp  33622  islpln2a  33648  lplncmp  33662  islvol2aN  33692  4at  33713  lvolcmp  33717  pmaple  33861  lncmp  33883  paddss  33945  llnexchb2lem  33968  2polcon4bN  34018  ispsubcl2N  34047  lhpat3  34146  lautcvr  34192  ltrnid  34235  trlval2  34264  trlatn0  34273  ltrnideq  34276  trlnidatb  34278  cdlemeg49lebilem  34641  trlord  34671  cdlemg1a  34672  cdlemg1cex  34690  tendoid0  34927  dva1dim  35087  cdlemm10N  35221  diarnN  35232  cdlemn  35315  dihlspsnssN  35435  dihatexv  35441  dochkrshp  35489  dochkrshp4  35492  djhlsmcl  35517  lcfl6  35603  lcfl8  35605  lcfrvalsnN  35644  lcfrlem9  35653  mapdval2N  35733  mapdordlem2  35740  mapd1o  35751  mapd0  35768  mapdheq2biN  35833  elrfi  36071  diophrw  36136  eldioph2b  36140  diophin  36150  rexrabdioph  36172  rmxycomplete  36296  coprmdvdsb  36366  jm2.19  36374  jm2.26  36383  jm2.27  36389  limsuc2  36425  dgraa0p  36534  rngunsnply  36558  fiuneneq  36590  pwelg  36680  nzss  37334  dvconstbi  37351  expgrowth  37352  bcc0  37357  axc11next  37425  pm14.24  37451  sbiota1  37453  sbcim2g  37565  sineq0ALT  37991  pwssfi  38032  elixpconstg  38090  eliuniin  38103  eliuniin2  38131  mapsnd  38179  mapss2  38188  fsneq  38189  fsneqrn  38194  mapssbi  38196  ssmapsn  38199  xralrple2  38308  infxrunb2  38322  xralrple4  38327  xralrple3  38328  xrralrecnnle  38340  xrralrecnnge  38351  reclt0  38352  iccintsng  38393  sqrlearg  38424  limcresiooub  38506  limclr  38519  climeldmeq  38529  dvnmul  38630  dvmptfprodlem  38631  ismbl3  38676  ismbl4  38683  fourierdlem50  38846  fourierdlem89  38885  fourierdlem91  38887  dfsalgen2  39032  sge0repnf  39076  sge0lefi  39088  sge0resplit  39096  sge0fodjrnlem  39106  voliunsge0lem  39162  hspdifhsp  39303  isvonmbl  39325  ovnovollem3  39345  vonvolmbl  39348  preimagelt  39386  preimalegt  39387  pimrecltpos  39393  preimaicomnf  39396  pimrecltneg  39407  issmflem  39410  issmfle  39429  issmfgt  39440  smfaddlem1  39446  issmfge  39453  smfresal  39470  sigarcol  39499  confun  39552  rexsb  39614  2reu2  39633  ralbinrald  39645  rlimdmafv  39704  el1fzopredsuc  39746  iccpartiun  39770  dfodd6  39886  dfeven4  39887  evensumeven  39952  sgoldbalt  40001  ccats1pfxeqbi  40092  reuccatpfxs1  40095  2ffzoeq  40181  uhgrauhgrbi  40289  uhgr0vb  40292  ausgrusgrb  40390  ushgredgedga  40451  ushgredgedgaloop  40453  usgr0vb  40458  usgr1v  40477  nbupgr  40561  nbumgrvtx  40563  nbuhgr2vtx1edgb  40569  edgusgrnbfin  40596  nb3grprlem1  40603  nbusgrvtxm1uvtx  40627  uvtxnbvtxm1  40628  cusgrfilem2  40667  uhgr0edg0rgrb  40769  cusgrm1rusgr  40777  spthonepeq-av  40953  usgr2pth  40965  1wlkiswwlks  41068  1wlkiswwlkupgr  41070  1wlklnwwlkn  41076  1wlklnwwlknupgr  41078  wwlksnextbi  41095  wwlksnredwwlkn0  41097  wwlksnextwrd  41098  wwlksnextprop  41113  wwlksnwwlksnon  41116  elwwlks2ons3  41154  umgrwwlks2on  41156  elwspths2on  41158  usgr2wspthons3  41162  elwwlks2  41165  elwspths2spth  41166  clwlkclwwlklem3  41205  clwwlksnun  41276  umgr3v3e3cycl  41346  eupth2lem3lem4  41394  frgr0v  41428  frgr3vlem2  41439  frgrncvvdeqlem3  41466  fusgr2wsp2nb  41493  isassintop  41631  uzlidlring  41714  rngciso  41769  rngcisoALTV  41781  ringciso  41820  ringcisoALTV  41844  domnmsuppn0  41939  lindslininds  42042  snlindsntor  42049  isldepslvec2  42063
  Copyright terms: Public domain W3C validator