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

Theorem impbid 201
Description: Deduce an equivalence from two implications. Deduction associated with impbi 197 and impbii 198. (Contributed by NM, 24-Jan-1993.) Revised to prove it from impbid21d 200. (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 200 . 2 (𝜑 → (𝜑 → (𝜓𝜒)))
43pm2.43i 50 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195
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 196
This theorem is referenced by:  bicom1  210  impbid1  214  impcon4bid  216  pm5.74  258  imbi1d  330  pm5.501  355  2falsed  365  impbida  873  dedlem0b  992  dedlema  993  dedlemb  994  albi  1736  alexbii  1750  exbiOLD  1763  equequ1  1939  equequ2  1940  elequ1  1984  elequ2  1991  19.21t  2061  sbequ12  2097  sb56  2136  19.21tOLD  2201  cbv2h  2257  dral1  2313  dral1ALT  2314  ax12b  2333  sbequ  2364  sbft  2367  exsb  2456  eupickb  2526  eupickbi  2527  2eu2  2542  eleq2dOLD  2674  ceqsalt  3201  ceqex  3303  mob2  3353  reu6  3362  sbciegft  3433  eqsbc3rOLD  3460  csbiebt  3519  sseq1  3589  reupick  3870  reupick2  3872  uneqdifeq  4009  uneqdifeqOLD  4010  eqoreldifOLD  4173  prnebg  4329  disjeq2  4557  disjeq1  4560  disjxiunOLD  4580  disjss3  4582  reusv2lem2  4795  reusv2lem2OLD  4796  reusv2lem3  4797  alxfr  4804  ralxfrd  4805  ralxfrdOLD  4806  ralxfrd2  4810  copsexg  4882  euotd  4900  poeq2  4963  sotric  4985  sotrieq  4986  freq2  5009  seeq1  5010  seeq2  5011  iss  5367  tz7.7  5666  ordtri1  5673  ordtri3OLD  5677  ordelinel  5742  ordelinelOLD  5743  iotaval  5779  funeq  5823  funssres  5844  f0dom0  6002  tz6.12c  6123  fnbrfvb  6146  ssimaex  6173  fvimacnv  6240  elpreima  6245  eldmrexrnb  6274  fsn  6308  fnsnb  6337  fmptsng  6339  fmptsnd  6340  tpres  6371  fconst2g  6373  fconst5  6376  elunirn  6413  f1ocnvfvb  6435  foeqcnvco  6455  f1eqcocnv  6456  fliftfun  6462  soisores  6477  isofr  6492  isose  6493  isopo  6496  isoso  6498  f1oiso2  6502  eusvobj2  6542  oprabid  6576  f1opw2  6786  oneqmin  6897  ordsuc  6906  ordelsuc  6912  ordsucelsuc  6914  ordunisuc2  6936  limsuc  6941  f1ovv  7030  op1steq  7101  fvn0elsuppb  7199  extmptsuppeq  7206  rntpos  7252  smoiso2  7353  seqomlem2  7433  oaord  7514  oawordex  7524  oaordex  7525  omord2  7534  om00  7542  oeord  7555  nnaord  7586  nnmord  7599  nnawordex  7604  nnaordex  7605  erexb  7654  swoord1  7660  swoord2  7661  iiner  7706  eceqoveq  7740  ralxpmap  7793  omxpenlem  7946  domtriord  7991  mapxpen  8011  mapunen  8014  ssenen  8019  nneneq  8028  onomeneq  8035  nndomo  8039  en1eqsnbi  8076  fodomfib  8125  f1opwfi  8153  fsuppunbi  8179  elfiun  8219  suplub2  8250  ordiso2  8303  ordiso  8304  oieu  8327  brwdom2  8361  brwdom3  8370  cantnflem1  8469  cardidm  8668  carddom2  8686  pm54.43  8709  pr2ne  8711  acnen  8759  acnen2  8761  alephord  8781  alephinit  8801  dfac5  8834  infdif2  8915  fictb  8950  coflim  8966  fincssdom  9028  fin23lem25  9029  isf32lem9  9066  isf34lem4  9082  fin1a2lem11  9115  axdc3lem2  9156  ficard  9266  fpwwe2lem12  9342  fpwwe2  9344  indpi  9608  nqereq  9636  1idpr  9730  ltapr  9746  leltne  10006  ltlen  10017  ltadd2  10020  addlsub  10326  addid0  10329  ltord1  10433  mul0or  10546  ltmul1  10752  mulge0b  10772  lt2msq  10787  negfi  10850  nnsub  10936  nn0sub  11220  zrevaddcl  11299  zltp1le  11304  zdiv  11323  nneo  11337  zeo2  11340  zmax  11661  zbtwnre  11662  qrevaddcl  11686  xrlttri  11848  xrleltne  11854  xralrple  11910  xltneg  11922  xleadd1  11957  xlemul1  11992  supxrunb1  12021  supxrunb2  12022  ioo0  12071  iccid  12091  ico0  12092  ioc0  12093  icc0  12094  difreicc  12175  iccsplit  12176  zltaddlt1le  12195  0fz1  12232  uzsplit  12281  fzm1  12289  fzrevral  12294  ssfzo12bi  12429  elfznelfzob  12440  flge  12468  modid2  12559  modmuladd  12574  ssnn0fi  12646  seqf1olem1  12702  hashen  12997  hashdom  13029  hash2exprb  13110  pr2pwpr  13116  hashtpg  13121  reuccats1  13332  ccats1swrdeqbi  13349  repsdf2  13376  scshwfzeqfzo  13423  relexpindlem  13651  shftlem  13656  shftuz  13657  abslt  13902  absle  13903  rexico  13941  cau3lem  13942  rlim2lt  14076  rlim3  14077  o1lo1  14116  rlimdm  14130  climshft  14155  o1dif  14208  isercolllem2  14244  isercoll  14246  zsum  14296  fsum  14298  fsum00  14371  incexclem  14407  zprod  14506  fprod  14510  dvdsval2  14824  moddvds  14829  negdvdsb  14836  dvdsnegb  14837  dvdscmulr  14848  dvdsmulcr  14849  dvdssub2  14861  dvdsaddre2b  14867  fzo0dvdseq  14883  mod2eq1n2dvds  14909  ltoddhalfle  14923  sumodd  14949  bitsf1ocnv  15004  sadcaddlem  15017  bitsuz  15034  dvdsgcdb  15100  gcdzeq  15109  dvdssqlem  15117  lcmeq0  15151  lcmdvdsb  15164  lcmfeq0b  15181  lcmf  15184  lcmfdvdsb  15194  coprmgcdb  15200  cncongr  15221  isprm2lem  15232  dvdsprime  15238  dvdsprm  15253  isprm7  15258  coprm  15261  euclemma  15263  rpexp  15270  prmdiveq  15329  hashgcdlem  15331  odzdvds  15338  pythagtrip  15377  pc2dvds  15421  pcprmpw2  15424  pcprmpw  15425  vdwapun  15516  ramtcl2  15553  firest  15916  mrieqv2d  16122  isacs2  16137  isssc  16303  setciso  16564  posasymb  16775  pleval2  16788  pltval3  16790  lublecllem  16811  joinle  16837  meetle  16851  lubun  16946  clatleglb  16949  latdisd  17013  letsr  17050  intopsn  17076  gsumval2a  17102  frmdss2  17223  isgrpid2  17281  isgrpinv  17295  symg1bas  17639  oddvdsnn0  17786  oddvds  17789  odeq  17792  odeq1  17800  gexdvds  17822  pgpfi  17843  pgpssslw  17852  fislw  17863  sylow3lem2  17866  lsmelvalm  17889  lsmlub  17901  lsmss1b  17903  lsmss2b  17905  efgs1b  17972  cyggenod  18109  cyggexb  18123  dprdfeq0  18244  ringinvnz1ne0  18415  ringinvnzdiv  18416  unitmulclb  18488  dvreq1  18516  f1rhm0to0  18563  f1rhm0to0ALT  18564  drngmul0or  18591  isabvd  18643  issrngd  18684  lssats2  18821  lspsneq0  18833  lsmelval2  18906  lvecvs0or  18929  lspsneq  18943  lspsneu  18944  lidl1el  19039  lidldvgen  19076  isnzr2  19084  0ringnnzr  19090  0ring01eqbi  19094  rrgeq0  19111  domneq0  19118  ply1coe1eq  19489  cply1coe0bi  19491  znunit  19731  psgndif  19767  ipeq0  19802  ocvsscon  19838  pjdm2  19874  obselocv  19891  islinds4  19993  mat1dimelbas  20096  cramer  20316  tgss3  20601  clsval2  20664  isopn3  20680  elcls3  20697  opncldf1  20698  neiint  20718  neips  20727  opnneissb  20728  opnssneib  20729  opnnei  20734  tpnei  20735  opnneiid  20740  restcld  20786  restopnb  20789  tgcn  20866  tgcnp  20867  subbascn  20868  iscnp4  20877  cnpnei  20878  cncls2  20887  cncls  20888  cnntr  20889  lmss  20912  hausnei2  20967  lpcls  20978  ordtt1  20993  cmpsub  21013  tgcmp  21014  1stcelcls  21074  locfincmp  21139  kgencn2  21170  ptpjpre1  21184  upxp  21236  txcn  21239  txlm  21261  tgqtop  21325  kqfvima  21343  isr0  21350  regr1lem2  21353  hmeoopn  21379  hmeocld  21380  ptuncnv  21420  fbunfip  21483  fgss2  21488  ufilb  21520  ufprim  21523  trufil  21524  cfinufil  21542  ufildr  21545  elfm2  21562  elfm3  21564  rnelfm  21567  fmfnfmlem4  21571  fmco  21575  flimtopon  21584  flimopn  21589  fbflim2  21591  flimrest  21597  flffbas  21609  cnpflf  21615  fclstopon  21626  fclsnei  21633  fclsbas  21635  fclsfnflim  21641  fclscmp  21644  ufilcmp  21646  isfcf  21648  fcfnei  21649  cnpfcf  21655  alexsubb  21660  alexsubALT  21665  cldsubg  21724  tgphaus  21730  tgpt0  21732  tsmsgsum  21752  tsmsres  21757  xbln0  22029  blssexps  22041  blssex  22042  isxms2  22063  prdsbl  22106  neibl  22116  metss  22123  met2ndc  22138  metrest  22139  metcnp3  22155  tngngp3  22270  nmoeq0  22350  xrsxmet  22420  reconn  22439  iccpnfcnv  22551  fgcfil  22877  iscau4  22885  cfilres  22902  iunmbl2  23132  ismbf3d  23227  mbfaddlem  23233  i1faddlem  23266  i1fmullem  23267  ellimc3  23449  tdeglem4  23624  deg1nn0clb  23654  deg1lt0  23655  dvdsq1p  23724  plypf1  23772  0dgrb  23806  plymul0or  23840  ulmshft  23948  ulmcaulem  23952  ulmcau  23953  cosord  24082  eff1olem  24098  lognegb  24140  eflogeq  24152  logdivlt  24171  efopn  24204  cxpeq0  24224  cxpeq  24298  angpieqvd  24358  dcubic  24373  asinsinb  24424  acoscosb  24425  atantanb  24451  rlimcnp  24492  isppw  24640  isppw2  24641  vmappw  24642  isnsqf  24661  ppieq0  24702  fsumdvdsdiag  24710  dvdsppwf1o  24712  fsumfldivdiag  24716  chpeq0  24733  chteq0  24734  dchrptlem1  24789  lgsdir2lem4  24853  lgsne0  24860  lgsqr  24876  lgsdchrval  24879  gausslemma2dlem1a  24890  lgsquadlem1  24905  m1lgs  24913  iscgrglt  25209  brbtwn  25579  brcgr  25580  brbtwn2  25585  axcontlem7  25650  uhgr0vb  25738  ausisusgra  25884  nbgraf1olem5  25974  edgusgranbfin  25979  nb3graprlem1  25980  cusgrarn  25988  nbcusgra  25992  cusgrafilem2  26008  uvtxnbgra  26021  uvtxnb  26025  spthonepeq  26117  3v3e3cycl  26193  wlkiswwlk  26226  wlklniswwlkn  26229  wwlknextbi  26253  wwlknredwwlkn0  26255  wwlkextwrd  26256  wwlkextprop  26272  0clwlk  26293  clwlkisclwwlklem0  26316  el2wlkonot  26396  el2spthonot  26397  el2wlkonotot0  26399  el2wlksotot  26409  usg2wlkonot  26410  usg2spthonot  26415  usg2spthonot0  26416  nbhashuvtx  26443  uvtxhashnb  26444  0eusgraiff0rgra  26466  cusgraiffrusgra  26467  eupath2lem3  26506  frgra3vlem2  26528  frgrancvvdeqlem3  26559  grpoinvf  26770  nvmul0or  26889  nvz  26908  diporthcom  26955  ubthlem3  27112  hvmul0or  27266  his6  27340  hial0  27343  hial02  27344  orthcom  27349  normgt0  27368  ocin  27539  occon3  27540  shsel3  27558  shlub  27657  chssoc  27739  h1de2bi  27797  spansncol  27811  elspansn4  27816  spansnss2  27818  sumspansn  27892  lnopcnbd  28279  lnfncnbd  28300  riesz1  28308  elpjrn  28433  cvcon3  28527  dmdmd  28543  dmdbr3  28548  dmdbr4  28549  dmdbr5  28551  mdslmd1i  28572  atcveq0  28591  chcv1  28598  atssma  28621  atcv0eq  28622  atcv1  28623  bian1d  28690  disjeq1f  28769  br8d  28802  fpwrelmap  28896  xaddeq0  28907  eliccelico  28929  elicoelioo  28930  isarchiofld  29148  unitdivcld  29275  xrge0iifcnv  29307  lmxrge0  29326  indf1ofs  29415  eulerpartlemgh  29767  dstfrvunirn  29863  bnj145OLD  30049  cvmliftmolem2  30518  cvmlift2lem12  30550  mthmb  30732  climuzcnv  30819  br8  30899  br6  30900  br4  30901  funbreq  30914  fprb  30916  axext4dist  30950  nodenselem8  31087  dfrdg4  31228  cgrcom  31267  cgrcoml  31273  cgrdegen  31281  btwncom  31291  brsegle  31385  brsegle2  31386  colinbtwnle  31395  btwnoutside  31402  broutsideof3  31403  outsidele  31409  lineunray  31424  lineelsb2  31425  elhf2  31452  elicc3  31481  nn0prpwlem  31487  opnbnd  31490  cldbnd  31491  opnregcld  31495  cldregopn  31496  fnessref  31522  refssfne  31523  neibastop2  31526  fnemeet2  31532  fnejoin2  31534  fgmin  31535  ontgval  31600  ordtop  31605  ordcmp  31616  nndivsub  31626  bj-ssbbi  31811  bj-ssbft  31831  bj-cbv2hv  31918  bj-dral1v  31936  bj-sbftv  31951  bj-equsal1t  31997  bj-19.21t  32005  bj-ceqsalt0  32067  bj-ceqsalt1  32068  bj-xpnzexb  32141  bj-xnex  32245  bj-finsumval0  32324  bj-ldiv  32332  bj-bary1  32339  isbasisrelowllem1  32379  isbasisrelowllem2  32380  finxpsuclem  32410  wl-lem-exsb  32527  wl-mo3t  32537  wl-ax11-lem1  32541  matunitlindf  32577  poimirlem6  32585  poimirlem7  32586  poimirlem16  32595  poimirlem19  32598  poimirlem22  32601  poimirlem23  32602  poimirlem24  32603  cnambfre  32628  itg2addnc  32634  brabg2  32680  istotbnd3  32740  sstotbnd2  32743  sstotbnd  32744  sstotbnd3  32745  ssbnd  32757  ismtybnd  32776  reheibor  32808  grpoeqdivid  32850  grpokerinj  32862  rngosn3  32893  rngoueqz  32909  1idl  32995  0rngo  32996  divrngidl  32997  igenval2  33035  ispridlc  33039  isdmn3  33043  prtlem10  33168  prter2  33184  dral1-o  33207  lshpinN  33294  lsatcveq0  33337  lsatcv0eq  33352  lsatcv1  33353  islshpcv  33358  lkr0f  33399  lkrshp4  33413  lshpkrlem1  33415  lshpset2N  33424  lfl1dim  33426  lfl1dim2N  33427  lub0N  33494  glb0N  33498  oplecon3b  33505  cmtcomN  33554  cmtbr3N  33559  cmtbr4N  33560  cvrnbtwn2  33580  cvrnbtwn3  33581  cvrcon3b  33582  cvrnbtwn4  33584  cvrcmp  33588  atcvreq0  33619  atnle  33622  atlatle  33625  cvlexchb1  33635  cvlcvr1  33644  hlrelat2  33707  exatleN  33708  cvrval3  33717  cvrval4N  33718  cvrexch  33724  atcvr0eq  33730  lnnat  33731  atcvrj0  33732  atcvrj2b  33736  atltcvr  33739  atbtwn  33750  ps-1  33781  3at  33794  islln2a  33821  llncmp  33826  islpln2a  33852  lplncmp  33866  islvol2aN  33896  4at  33917  lvolcmp  33921  pmaple  34065  lncmp  34087  paddss  34149  llnexchb2lem  34172  2polcon4bN  34222  ispsubcl2N  34251  lhpat3  34350  lautcvr  34396  ltrnid  34439  trlval2  34468  trlatn0  34477  ltrnideq  34480  trlnidatb  34482  cdlemeg49lebilem  34845  trlord  34875  cdlemg1a  34876  cdlemg1cex  34894  tendoid0  35131  dva1dim  35291  cdlemm10N  35425  diarnN  35436  cdlemn  35519  dihlspsnssN  35639  dihatexv  35645  dochkrshp  35693  dochkrshp4  35696  djhlsmcl  35721  lcfl6  35807  lcfl8  35809  lcfrvalsnN  35848  lcfrlem9  35857  mapdval2N  35937  mapdordlem2  35944  mapd1o  35955  mapd0  35972  mapdheq2biN  36037  elrfi  36275  diophrw  36340  eldioph2b  36344  diophin  36354  rexrabdioph  36376  rmxycomplete  36500  coprmdvdsb  36570  jm2.19  36578  jm2.26  36587  jm2.27  36593  limsuc2  36629  dgraa0p  36738  rngunsnply  36762  fiuneneq  36794  pwelg  36884  nzss  37538  dvconstbi  37555  expgrowth  37556  bcc0  37561  axc11next  37629  pm14.24  37655  sbiota1  37657  sbcim2g  37769  sineq0ALT  38195  pwssfi  38236  elixpconstg  38294  eliuniin  38307  eliuniin2  38335  mapsnd  38383  mapss2  38392  fsneq  38393  fsneqrn  38398  mapssbi  38400  ssmapsn  38403  xralrple2  38511  infxrunb2  38525  xralrple4  38530  xralrple3  38531  xrralrecnnle  38543  xrralrecnnge  38554  reclt0  38555  iccintsng  38596  sqrlearg  38627  limcresiooub  38709  limclr  38722  climeldmeq  38732  dvnmul  38833  dvmptfprodlem  38834  ismbl3  38879  ismbl4  38886  fourierdlem50  39049  fourierdlem89  39088  fourierdlem91  39090  dfsalgen2  39235  sge0repnf  39279  sge0lefi  39291  sge0resplit  39299  sge0fodjrnlem  39309  voliunsge0lem  39365  hspdifhsp  39506  isvonmbl  39528  ovnovollem3  39548  vonvolmbl  39551  preimagelt  39589  preimalegt  39590  pimrecltpos  39596  preimaicomnf  39599  pimrecltneg  39610  issmflem  39613  issmfle  39632  issmfgt  39643  smfaddlem1  39649  issmfge  39656  smfresal  39673  sigarcol  39702  confun  39755  rexsb  39817  2reu2  39836  ralbinrald  39848  rlimdmafv  39906  el1fzopredsuc  39948  iccpartiun  39972  dfodd6  40088  dfeven4  40089  evensumeven  40154  sgoldbalt  40203  ccats1pfxeqbi  40294  reuccatpfxs1  40297  2ffzoeq  40361  uhgrauhgrbi  40377  ausgrusgrb  40395  ushgredgedga  40456  ushgredgedgaloop  40458  usgr0vb  40463  usgr1v  40482  nbupgr  40566  nbumgrvtx  40568  nbuhgr2vtx1edgb  40574  edgusgrnbfin  40601  nb3grprlem1  40608  nbusgrvtxm1uvtx  40632  uvtxnbvtxm1  40633  cusgrfilem2  40672  uhgr0edg0rgrb  40774  cusgrm1rusgr  40782  spthonepeq-av  40958  usgr2pth  40970  1wlkiswwlks  41073  1wlkiswwlkupgr  41075  1wlklnwwlkn  41081  1wlklnwwlknupgr  41083  wwlksnextbi  41100  wwlksnredwwlkn0  41102  wwlksnextwrd  41103  wwlksnextprop  41118  wwlksnwwlksnon  41121  elwwlks2ons3  41159  umgrwwlks2on  41161  elwspths2on  41163  usgr2wspthons3  41167  elwwlks2  41170  elwspths2spth  41171  clwlkclwwlklem3  41210  clwwlksnun  41281  umgr3v3e3cycl  41351  eupth2lem3lem4  41399  frgr0v  41433  frgr3vlem2  41444  frgrncvvdeqlem3  41471  fusgr2wsp2nb  41498  isassintop  41636  uzlidlring  41719  rngciso  41774  rngcisoALTV  41786  ringciso  41825  ringcisoALTV  41849  domnmsuppn0  41944  lindslininds  42047  snlindsntor  42054  isldepslvec2  42068
  Copyright terms: Public domain W3C validator