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  895  dedlem0b  1013  dedlema  1014  dedlemb  1015  albi  1786  alexbii  1800  equequ1  1998  equequ2  1999  elequ1  2037  elequ2  2044  19.21tOLDOLD  2112  sbequ12  2149  sb56  2188  19.21tOLD  2249  cbv2h  2305  dral1  2356  dral1ALT  2357  ax12b  2373  sbequ  2404  sbft  2407  exsb  2496  eupickb  2567  eupickbi  2568  2eu2  2583  ceqsalt  3259  rspcebdv  3345  ceqex  3364  mob2  3419  reu6  3428  sbciegft  3499  eqsbc3rOLD  3526  csbiebt  3586  sseq1  3659  ssdifsym  3896  reupick  3944  reupick2  3946  uneqdifeq  4090  uneqdifeqOLD  4091  eqoreldifOLD  4258  prnebg  4420  disjeq2  4656  disjeq1  4659  disjxiunOLD  4682  disjss3  4684  reusv2lem2  4899  reusv2lem2OLD  4900  reusv2lem3  4901  alxfr  4908  ralxfrd  4909  ralxfrdOLD  4910  ralxfrd2  4914  copsexg  4985  euotd  5004  poeq2  5068  sotric  5090  sotrieq  5091  freq2  5114  seeq1  5115  seeq2  5116  iss  5482  tz7.7  5787  ordtri1  5794  ordtri3OLD  5798  ordelinel  5863  ordelinelOLD  5864  iotaval  5900  funeq  5946  funssres  5968  f0dom0  6127  tz6.12c  6251  fnbrfvb  6274  ssimaex  6302  fvimacnv  6372  elpreima  6377  eldmrexrnb  6406  fsn  6442  fnsnb  6473  fmptsng  6475  fmptsnd  6476  tpres  6507  fconst2g  6509  fconst5  6512  elunirn  6549  f1ocnvfvb  6575  foeqcnvco  6595  f1eqcocnv  6596  fliftfun  6602  soisores  6617  isofr  6632  isose  6633  isopo  6636  isoso  6638  f1oiso2  6642  eusvobj2  6683  oprabid  6717  f1opw2  6930  oneqmin  7047  ordsuc  7056  ordelsuc  7062  ordsucelsuc  7064  ordunisuc2  7086  limsuc  7091  f1ovv  7179  op1steq  7254  fvn0elsuppb  7357  extmptsuppeq  7364  rntpos  7410  smoiso2  7511  seqomlem2  7591  oaord  7672  oawordex  7682  oaordex  7683  omord2  7692  om00  7700  oeord  7713  nnaord  7744  nnmord  7757  nnawordex  7762  nnaordex  7763  erexb  7812  swoord1  7818  swoord2  7819  iiner  7862  eceqoveq  7895  ralxpmap  7949  omxpenlem  8102  domtriord  8147  mapxpen  8167  mapunen  8170  ssenen  8175  nneneq  8184  onomeneq  8191  nndomo  8195  en1eqsnbi  8232  fodomfib  8281  f1opwfi  8311  fsuppunbi  8337  elfiun  8377  suplub2  8408  ordiso2  8461  ordiso  8462  oieu  8485  brwdom2  8519  brwdom3  8528  cantnflem1  8624  cardidm  8823  carddom2  8841  pm54.43  8864  pr2ne  8866  acnen  8914  acnen2  8916  alephord  8936  alephinit  8956  dfac5  8989  infdif2  9070  fictb  9105  coflim  9121  fincssdom  9183  fin23lem25  9184  isf32lem9  9221  isf34lem4  9237  fin1a2lem11  9270  axdc3lem2  9311  ficard  9425  fpwwe2lem12  9501  fpwwe2  9503  indpi  9767  nqereq  9795  1idpr  9889  ltapr  9905  leltne  10165  ltlen  10176  ltadd2  10179  addlsub  10485  addid0  10488  ltord1  10592  mul0or  10705  ltmul1  10911  mulge0b  10931  lt2msq  10946  negfi  11009  nnsub  11097  nn0sub  11381  zrevaddcl  11460  zltp1le  11465  zdiv  11485  nneo  11499  zeo2  11502  zmax  11823  zbtwnre  11824  qrevaddcl  11848  xrlttri  12010  xrleltne  12016  xralrple  12074  xltneg  12086  xleadd1  12123  xlemul1  12158  supxrunb1  12187  supxrunb2  12188  ioo0  12238  iccid  12258  ico0  12259  ioc0  12260  icc0  12261  difreicc  12342  iccsplit  12343  zltaddlt1le  12362  0fz1  12399  uzsplit  12450  fzm1  12458  fzrevral  12463  ssfzo12bi  12603  elfznelfzob  12614  flge  12646  modid2  12737  modmuladd  12752  ssnn0fi  12824  seqf1olem1  12880  hashen  13175  hashdom  13206  hash2exprb  13291  pr2pwpr  13299  hashtpg  13305  len0nnbi  13373  reuccats1  13526  ccats1swrdeqbi  13544  repsdf2  13571  scshwfzeqfzo  13618  relexpindlem  13847  shftlem  13852  shftuz  13853  abslt  14098  absle  14099  rexico  14137  cau3lem  14138  rlim2lt  14272  rlim3  14273  o1lo1  14312  rlimdm  14326  climshft  14351  o1dif  14404  isercolllem2  14440  isercoll  14442  zsum  14493  fsum  14495  fsum00  14574  incexclem  14612  zprod  14711  fprod  14715  dvdsval2  15030  moddvds  15038  negdvdsb  15045  dvdsnegb  15046  dvdscmulr  15057  dvdsmulcr  15058  dvdssub2  15070  dvdsaddre2b  15076  fzo0dvdseq  15092  mod2eq1n2dvds  15118  ltoddhalfle  15132  sumodd  15158  bitsf1ocnv  15213  sadcaddlem  15226  bitsuz  15243  dvdsgcdb  15309  gcdzeq  15318  dvdssqlem  15326  lcmeq0  15360  lcmdvdsb  15373  lcmfeq0b  15390  lcmf  15393  lcmfdvdsb  15403  coprmgcdb  15409  cncongr  15430  isprm2lem  15441  dvdsprime  15447  dvdsprm  15462  isprm7  15467  coprm  15470  euclemma  15472  rpexp  15479  prmdiveq  15538  hashgcdlem  15540  odzdvds  15547  pythagtrip  15586  pc2dvds  15630  pcprmpw2  15633  pcprmpw  15634  vdwapun  15725  ramtcl2  15762  firest  16140  mrieqv2d  16346  isacs2  16361  isssc  16527  setciso  16788  posasymb  16999  pleval2  17012  pltval3  17014  lublecllem  17035  joinle  17061  meetle  17075  lubun  17170  clatleglb  17173  latdisd  17237  letsr  17274  intopsn  17300  gsumval2a  17326  frmdss2  17447  isgrpid2  17505  isgrpinv  17519  symg1bas  17862  oddvdsnn0  18009  oddvds  18012  odeq  18015  odeq1  18023  gexdvds  18045  pgpfi  18066  pgpssslw  18075  fislw  18086  sylow3lem2  18089  lsmelvalm  18112  lsmlub  18124  lsmss1b  18126  lsmss2b  18128  efgs1b  18195  cyggenod  18332  cyggexb  18346  dprdfeq0  18467  ringinvnz1ne0  18638  ringinvnzdiv  18639  unitmulclb  18711  dvreq1  18739  f1rhm0to0  18788  f1rhm0to0ALT  18789  drngmul0or  18816  isabvd  18868  issrngd  18909  lssats2  19048  lspsneq0  19060  lsmelval2  19133  lvecvs0or  19156  lspsneq  19170  lspsneu  19171  lidl1el  19266  lidldvgen  19303  isnzr2  19311  0ringnnzr  19317  0ring01eqbi  19321  rrgeq0  19338  domneq0  19345  ply1coe1eq  19716  cply1coe0bi  19718  znunit  19960  psgndif  19996  ipeq0  20031  ocvsscon  20067  pjdm2  20103  obselocv  20120  islinds4  20222  mat1dimelbas  20325  cramer  20545  toponcomb  20781  tgss3  20838  clsval2  20902  isopn3  20918  elcls3  20935  opncldf1  20936  neiint  20956  neips  20965  opnneissb  20966  opnssneib  20967  opnnei  20972  tpnei  20973  opnneiid  20978  restcld  21024  restopnb  21027  tgcn  21104  tgcnp  21105  subbascn  21106  iscnp4  21115  cnpnei  21116  cncls2  21125  cncls  21126  cnntr  21127  lmss  21150  hausnei2  21205  lpcls  21216  ordtt1  21231  cmpsub  21251  tgcmp  21252  1stcelcls  21312  locfincmp  21377  kgencn2  21408  ptpjpre1  21422  upxp  21474  txcn  21477  txlm  21499  tgqtop  21563  kqfvima  21581  isr0  21588  regr1lem2  21591  hmeoopn  21617  hmeocld  21618  ptuncnv  21658  fbunfip  21720  fgss2  21725  ufilb  21757  ufprim  21760  trufil  21761  cfinufil  21779  ufildr  21782  elfm2  21799  elfm3  21801  rnelfm  21804  fmfnfmlem4  21808  fmco  21812  flimtopon  21821  flimopn  21826  fbflim2  21828  flimrest  21834  flffbas  21846  cnpflf  21852  fclstopon  21863  fclsnei  21870  fclsbas  21872  fclsfnflim  21878  fclscmp  21881  ufilcmp  21883  isfcf  21885  fcfnei  21886  cnpfcf  21892  alexsubb  21897  alexsubALT  21902  cldsubg  21961  tgphaus  21967  tgpt0  21969  tsmsgsum  21989  tsmsres  21994  xbln0  22266  blssexps  22278  blssex  22279  isxms2  22300  prdsbl  22343  neibl  22353  metss  22360  met2ndc  22375  metrest  22376  metcnp3  22392  tngngp3  22507  nmoeq0  22587  xrsxmet  22659  reconn  22678  iccpnfcnv  22790  fgcfil  23115  iscau4  23123  cfilres  23140  iunmbl2  23371  ismbf3d  23466  mbfaddlem  23472  i1faddlem  23505  i1fmullem  23506  ellimc3  23688  tdeglem4  23865  deg1nn0clb  23895  deg1lt0  23896  dvdsq1p  23965  plypf1  24013  0dgrb  24047  plymul0or  24081  ulmshft  24189  ulmcaulem  24193  ulmcau  24194  cosord  24323  eff1olem  24339  lognegb  24381  eflogeq  24393  logdivlt  24412  efopn  24449  cxpeq0  24469  cxpeq  24543  angpieqvd  24603  dcubic  24618  asinsinb  24669  acoscosb  24670  atantanb  24696  rlimcnp  24737  isppw  24885  isppw2  24886  vmappw  24887  isnsqf  24906  ppieq0  24947  fsumdvdsdiag  24955  dvdsppwf1o  24957  fsumfldivdiag  24961  chpeq0  24978  chteq0  24979  dchrptlem1  25034  lgsdir2lem4  25098  lgsne0  25105  lgsqr  25121  lgsdchrval  25124  gausslemma2dlem1a  25135  lgsquadlem1  25150  m1lgs  25158  iscgrglt  25454  brbtwn  25824  brcgr  25825  brbtwn2  25830  axcontlem7  25895  uhgr0vb  26012  edglnl  26083  ausgrusgrb  26105  ushgredgedg  26166  ushgredgedgloop  26168  usgr0vb  26174  usgr1v  26193  nbupgr  26285  nbumgrvtx  26287  nbuhgr2vtx1edgb  26293  edgusgrnbfin  26319  nb3grprlem1  26326  uvtxnbvtxm1  26357  cusgrfilem2  26408  uhgr0edg0rgrb  26526  cusgrm1rusgr  26534  spthonepeq  26704  usgr2pth  26716  wlkiswwlks  26830  wlkiswwlkupgr  26832  wlklnwwlkn  26838  wlklnwwlknupgr  26840  wwlksnextbi  26857  wwlksnredwwlkn0  26859  wwlksnextwrd  26860  wwlksnextprop  26875  wwlksnwwlksnonOLD  26880  elwwlks2ons3OLD  26921  umgrwwlks2on  26923  elwspths2on  26926  usgr2wspthons3  26931  elwwlks2  26933  elwspths2spth  26934  clwlkclwwlklem3  26967  loopclwwlkn1b  27005  clwwlknon1sn  27075  clwwlknonwwlknonb  27080  clwwlknonwwlknonbOLD  27081  clwwlknunOLD  27091  umgr3v3e3cycl  27162  eupth2lem3lem4  27209  frgr0v  27241  frgr3vlem2  27254  2clwwlk2clwwlk  27338  grpoinvf  27514  nvmul0or  27633  nvz  27652  diporthcom  27699  ubthlem3  27856  hvmul0or  28010  his6  28084  hial0  28087  hial02  28088  orthcom  28093  normgt0  28112  ocin  28283  occon3  28284  shsel3  28302  shlub  28401  chssoc  28483  h1de2bi  28541  spansncol  28555  elspansn4  28560  spansnss2  28562  sumspansn  28636  lnopcnbd  29023  lnfncnbd  29044  riesz1  29052  elpjrn  29177  cvcon3  29271  dmdmd  29287  dmdbr3  29292  dmdbr4  29293  dmdbr5  29295  mdslmd1i  29316  atcveq0  29335  chcv1  29342  atssma  29365  atcv0eq  29366  atcv1  29367  bian1d  29434  disjeq1f  29513  br8d  29548  fpwrelmap  29636  xaddeq0  29646  eliccelico  29667  elicoelioo  29668  isarchiofld  29945  unitdivcld  30075  xrge0iifcnv  30107  lmxrge0  30126  indf1ofs  30216  eulerpartlemgh  30568  dstfrvunirn  30664  cvmliftmolem2  31390  cvmlift2lem12  31422  mthmb  31604  climuzcnv  31691  br8  31772  br6  31773  br4  31774  funbreq  31794  fprb  31795  axext4dist  31830  nodenselem8  31966  dfrdg4  32183  cgrcom  32222  cgrcoml  32228  cgrdegen  32236  btwncom  32246  brsegle  32340  brsegle2  32341  colinbtwnle  32350  btwnoutside  32357  broutsideof3  32358  outsidele  32364  lineunray  32379  lineelsb2  32380  elhf2  32407  elicc3  32436  nn0prpwlem  32442  opnbnd  32445  cldbnd  32446  opnregcld  32450  cldregopn  32451  fnessref  32477  refssfne  32478  neibastop2  32481  fnemeet2  32487  fnejoin2  32489  fgmin  32490  ontgval  32555  ordtop  32560  ordcmp  32571  nndivsub  32581  bj-ssbbi  32747  bj-ssbft  32767  bj-cbv2hv  32856  bj-dral1v  32873  bj-sbftv  32888  bj-equsal1t  32934  bj-19.21t  32942  bj-ceqsalt0  32998  bj-ceqsalt1  32999  bj-xpnzexb  33073  bj-finsumval0  33277  bj-ldiv  33285  bj-bary1  33292  dfgcd3  33300  isbasisrelowllem1  33333  isbasisrelowllem2  33334  finxpsuclem  33364  wl-lem-exsb  33478  wl-mo3t  33488  wl-ax11-lem1  33492  wl-clelv2-just  33509  matunitlindf  33537  poimirlem6  33545  poimirlem7  33546  poimirlem16  33555  poimirlem19  33558  poimirlem22  33561  poimirlem23  33562  poimirlem24  33563  cnambfre  33588  itg2addnc  33594  brabg2  33640  istotbnd3  33700  sstotbnd2  33703  sstotbnd  33704  sstotbnd3  33705  ssbnd  33717  ismtybnd  33736  reheibor  33768  grpoeqdivid  33810  grpokerinj  33822  rngosn3  33853  rngoueqz  33869  1idl  33955  0rngo  33956  divrngidl  33957  igenval2  33995  ispridlc  33999  isdmn3  34003  relcnveq3  34233  iss2  34252  elrelscnveq3  34381  prtlem10  34469  prter2  34485  dral1-o  34508  lshpinN  34594  lsatcveq0  34637  lsatcv0eq  34652  lsatcv1  34653  islshpcv  34658  lkr0f  34699  lkrshp4  34713  lshpkrlem1  34715  lshpset2N  34724  lfl1dim  34726  lfl1dim2N  34727  lub0N  34794  glb0N  34798  oplecon3b  34805  cmtcomN  34854  cmtbr3N  34859  cmtbr4N  34860  cvrnbtwn2  34880  cvrnbtwn3  34881  cvrcon3b  34882  cvrnbtwn4  34884  cvrcmp  34888  atcvreq0  34919  atnle  34922  atlatle  34925  cvlexchb1  34935  cvlcvr1  34944  hlrelat2  35007  exatleN  35008  cvrval3  35017  cvrval4N  35018  cvrexch  35024  atcvr0eq  35030  lnnat  35031  atcvrj0  35032  atcvrj2b  35036  atltcvr  35039  atbtwn  35050  ps-1  35081  3at  35094  islln2a  35121  llncmp  35126  islpln2a  35152  lplncmp  35166  islvol2aN  35196  4at  35217  lvolcmp  35221  pmaple  35365  lncmp  35387  paddss  35449  llnexchb2lem  35472  2polcon4bN  35522  ispsubcl2N  35551  lhpat3  35650  lautcvr  35696  ltrnid  35739  trlval2  35768  trlatn0  35777  ltrnideq  35780  trlnidatb  35782  cdlemeg49lebilem  36144  trlord  36174  cdlemg1a  36175  cdlemg1cex  36193  tendoid0  36430  dva1dim  36590  cdlemm10N  36724  diarnN  36735  cdlemn  36818  dihlspsnssN  36938  dihatexv  36944  dochkrshp  36992  dochkrshp4  36995  djhlsmcl  37020  lcfl6  37106  lcfl8  37108  lcfrvalsnN  37147  lcfrlem9  37156  mapdval2N  37236  mapdordlem2  37243  mapd1o  37254  mapd0  37271  mapdheq2biN  37336  elrfi  37574  diophrw  37639  eldioph2b  37643  diophin  37653  rexrabdioph  37675  rmxycomplete  37799  coprmdvdsb  37869  jm2.19  37877  jm2.26  37886  jm2.27  37892  limsuc2  37928  dgraa0p  38036  rngunsnply  38060  fiuneneq  38092  pwelg  38182  nzss  38833  dvconstbi  38850  expgrowth  38851  bcc0  38856  axc11next  38924  pm14.24  38950  sbiota1  38952  sbcim2g  39065  sineq0ALT  39487  pwssfi  39525  elixpconstg  39580  mapsnd  39702  mapss2  39711  fsneq  39712  fsneqrn  39717  mapssbi  39719  ssmapsn  39722  rnmptbd2lem  39777  infnsuprnmpt  39779  rnmptbdlem  39784  xralrple2  39883  infxrunb2  39897  xralrple4  39902  xralrple3  39903  xrralrecnnle  39915  xrralrecnnge  39926  reclt0  39927  supxrunb3  39936  supxrleubrnmpt  39945  xrre4  39951  unb2ltle  39955  rexabslelem  39958  suprleubrnmpt  39962  infxrunb3rnmpt  39968  uzub  39971  supminfrnmpt  39985  iccintsng  40067  sqrlearg  40098  uzinico  40105  preimaiocmnf  40106  limcresiooub  40192  limclr  40205  climeldmeq  40215  limsuppnflem  40260  limsupmnflem  40270  limsupmnfuzlem  40276  limsupre3lem  40282  limsupre3uzlem  40285  liminfreuzlem  40352  dvnmul  40476  dvmptfprodlem  40477  ismbl3  40521  ismbl4  40528  fourierdlem50  40691  fourierdlem89  40730  fourierdlem91  40732  dfsalgen2  40877  sge0repnf  40921  sge0lefi  40933  sge0resplit  40941  sge0fodjrnlem  40951  voliunsge0lem  41007  hspdifhsp  41151  isvonmbl  41173  ovnovollem3  41193  vonvolmbl  41196  preimagelt  41233  preimalegt  41234  pimrecltpos  41240  preimaicomnf  41243  pimrecltneg  41254  issmflem  41257  issmfle  41275  issmfgt  41286  smfaddlem1  41292  issmfge  41299  smfresal  41316  smflimmpt  41337  smfinflem  41344  smflimsuplem7  41353  smflimsupmpt  41356  sigarcol  41374  confun  41427  rexsb  41489  2reu2  41508  ralbinrald  41520  rlimdmafv  41578  el1fzopredsuc  41660  2ffzoeq  41663  iccpartiun  41695  ccats1pfxeqbi  41756  reuccatpfxs1  41759  dfodd6  41875  dfeven4  41876  evensumeven  41941  sbgoldbalt  41994  sprsymrelfolem2  42068  isassintop  42171  uzlidlring  42254  rngciso  42307  rngcisoALTV  42319  ringciso  42358  ringcisoALTV  42382  domnmsuppn0  42475  lindslininds  42578  snlindsntor  42585  isldepslvec2  42599
  Copyright terms: Public domain W3C validator