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  331  pm5.501  356  2falsed  366  impbida  876  dedlem0b  1000  dedlema  1001  dedlemb  1002  albi  1743  alexbii  1757  equequ1  1949  equequ2  1950  elequ1  1994  elequ2  2001  19.21tOLDOLD  2072  sbequ12  2108  sb56  2147  19.21tOLD  2212  cbv2h  2268  dral1  2324  dral1ALT  2325  ax12b  2344  sbequ  2375  sbft  2378  exsb  2467  eupickb  2537  eupickbi  2538  2eu2  2553  ceqsalt  3218  ceqex  3321  mob2  3373  reu6  3382  sbciegft  3453  eqsbc3rOLD  3480  csbiebt  3539  sseq1  3611  reupick  3893  reupick2  3895  uneqdifeq  4035  uneqdifeqOLD  4036  eqoreldifOLD  4204  prnebg  4364  disjeq2  4597  disjeq1  4600  disjxiunOLD  4620  disjss3  4622  reusv2lem2  4839  reusv2lem2OLD  4840  reusv2lem3  4841  alxfr  4848  ralxfrd  4849  ralxfrdOLD  4850  ralxfrd2  4854  copsexg  4926  euotd  4945  poeq2  5009  sotric  5031  sotrieq  5032  freq2  5055  seeq1  5056  seeq2  5057  iss  5416  tz7.7  5718  ordtri1  5725  ordtri3OLD  5729  ordelinel  5794  ordelinelOLD  5795  iotaval  5831  funeq  5877  funssres  5898  f0dom0  6056  tz6.12c  6180  fnbrfvb  6203  ssimaex  6230  fvimacnv  6298  elpreima  6303  eldmrexrnb  6332  fsn  6367  fnsnb  6397  fmptsng  6399  fmptsnd  6400  tpres  6431  fconst2g  6433  fconst5  6436  elunirn  6474  f1ocnvfvb  6500  foeqcnvco  6520  f1eqcocnv  6521  fliftfun  6527  soisores  6542  isofr  6557  isose  6558  isopo  6561  isoso  6563  f1oiso2  6567  eusvobj2  6608  oprabid  6642  f1opw2  6853  abnex  6929  oneqmin  6967  ordsuc  6976  ordelsuc  6982  ordsucelsuc  6984  ordunisuc2  7006  limsuc  7011  f1ovv  7099  op1steq  7170  fvn0elsuppb  7272  extmptsuppeq  7279  rntpos  7325  smoiso2  7426  seqomlem2  7506  oaord  7587  oawordex  7597  oaordex  7598  omord2  7607  om00  7615  oeord  7628  nnaord  7659  nnmord  7672  nnawordex  7677  nnaordex  7678  erexb  7727  swoord1  7733  swoord2  7734  iiner  7779  eceqoveq  7813  ralxpmap  7867  omxpenlem  8021  domtriord  8066  mapxpen  8086  mapunen  8089  ssenen  8094  nneneq  8103  onomeneq  8110  nndomo  8114  en1eqsnbi  8151  fodomfib  8200  f1opwfi  8230  fsuppunbi  8256  elfiun  8296  suplub2  8327  ordiso2  8380  ordiso  8381  oieu  8404  brwdom2  8438  brwdom3  8447  cantnflem1  8546  cardidm  8745  carddom2  8763  pm54.43  8786  pr2ne  8788  acnen  8836  acnen2  8838  alephord  8858  alephinit  8878  dfac5  8911  infdif2  8992  fictb  9027  coflim  9043  fincssdom  9105  fin23lem25  9106  isf32lem9  9143  isf34lem4  9159  fin1a2lem11  9192  axdc3lem2  9233  ficard  9347  fpwwe2lem12  9423  fpwwe2  9425  indpi  9689  nqereq  9717  1idpr  9811  ltapr  9827  leltne  10087  ltlen  10098  ltadd2  10101  addlsub  10407  addid0  10410  ltord1  10514  mul0or  10627  ltmul1  10833  mulge0b  10853  lt2msq  10868  negfi  10931  nnsub  11019  nn0sub  11303  zrevaddcl  11382  zltp1le  11387  zdiv  11407  nneo  11421  zeo2  11424  zmax  11745  zbtwnre  11746  qrevaddcl  11770  xrlttri  11932  xrleltne  11938  xralrple  11995  xltneg  12007  xleadd1  12044  xlemul1  12079  supxrunb1  12108  supxrunb2  12109  ioo0  12158  iccid  12178  ico0  12179  ioc0  12180  icc0  12181  difreicc  12262  iccsplit  12263  zltaddlt1le  12282  0fz1  12319  uzsplit  12369  fzm1  12377  fzrevral  12382  ssfzo12bi  12520  elfznelfzob  12531  flge  12562  modid2  12653  modmuladd  12668  ssnn0fi  12740  seqf1olem1  12796  hashen  13091  hashdom  13124  hash2exprb  13207  pr2pwpr  13215  hashtpg  13221  reuccats1  13434  ccats1swrdeqbi  13451  repsdf2  13478  scshwfzeqfzo  13525  relexpindlem  13753  shftlem  13758  shftuz  13759  abslt  14004  absle  14005  rexico  14043  cau3lem  14044  rlim2lt  14178  rlim3  14179  o1lo1  14218  rlimdm  14232  climshft  14257  o1dif  14310  isercolllem2  14346  isercoll  14348  zsum  14398  fsum  14400  fsum00  14476  incexclem  14512  zprod  14611  fprod  14615  dvdsval2  14929  moddvds  14934  negdvdsb  14941  dvdsnegb  14942  dvdscmulr  14953  dvdsmulcr  14954  dvdssub2  14966  dvdsaddre2b  14972  fzo0dvdseq  14988  mod2eq1n2dvds  15014  ltoddhalfle  15028  sumodd  15054  bitsf1ocnv  15109  sadcaddlem  15122  bitsuz  15139  dvdsgcdb  15205  gcdzeq  15214  dvdssqlem  15222  lcmeq0  15256  lcmdvdsb  15269  lcmfeq0b  15286  lcmf  15289  lcmfdvdsb  15299  coprmgcdb  15305  cncongr  15326  isprm2lem  15337  dvdsprime  15343  dvdsprm  15358  isprm7  15363  coprm  15366  euclemma  15368  rpexp  15375  prmdiveq  15434  hashgcdlem  15436  odzdvds  15443  pythagtrip  15482  pc2dvds  15526  pcprmpw2  15529  pcprmpw  15530  vdwapun  15621  ramtcl2  15658  firest  16033  mrieqv2d  16239  isacs2  16254  isssc  16420  setciso  16681  posasymb  16892  pleval2  16905  pltval3  16907  lublecllem  16928  joinle  16954  meetle  16968  lubun  17063  clatleglb  17066  latdisd  17130  letsr  17167  intopsn  17193  gsumval2a  17219  frmdss2  17340  isgrpid2  17398  isgrpinv  17412  symg1bas  17756  oddvdsnn0  17903  oddvds  17906  odeq  17909  odeq1  17917  gexdvds  17939  pgpfi  17960  pgpssslw  17969  fislw  17980  sylow3lem2  17983  lsmelvalm  18006  lsmlub  18018  lsmss1b  18020  lsmss2b  18022  efgs1b  18089  cyggenod  18226  cyggexb  18240  dprdfeq0  18361  ringinvnz1ne0  18532  ringinvnzdiv  18533  unitmulclb  18605  dvreq1  18633  f1rhm0to0  18680  f1rhm0to0ALT  18681  drngmul0or  18708  isabvd  18760  issrngd  18801  lssats2  18940  lspsneq0  18952  lsmelval2  19025  lvecvs0or  19048  lspsneq  19062  lspsneu  19063  lidl1el  19158  lidldvgen  19195  isnzr2  19203  0ringnnzr  19209  0ring01eqbi  19213  rrgeq0  19230  domneq0  19237  ply1coe1eq  19608  cply1coe0bi  19610  znunit  19852  psgndif  19888  ipeq0  19923  ocvsscon  19959  pjdm2  19995  obselocv  20012  islinds4  20114  mat1dimelbas  20217  cramer  20437  toponcomb  20673  tgss3  20730  clsval2  20794  isopn3  20810  elcls3  20827  opncldf1  20828  neiint  20848  neips  20857  opnneissb  20858  opnssneib  20859  opnnei  20864  tpnei  20865  opnneiid  20870  restcld  20916  restopnb  20919  tgcn  20996  tgcnp  20997  subbascn  20998  iscnp4  21007  cnpnei  21008  cncls2  21017  cncls  21018  cnntr  21019  lmss  21042  hausnei2  21097  lpcls  21108  ordtt1  21123  cmpsub  21143  tgcmp  21144  1stcelcls  21204  locfincmp  21269  kgencn2  21300  ptpjpre1  21314  upxp  21366  txcn  21369  txlm  21391  tgqtop  21455  kqfvima  21473  isr0  21480  regr1lem2  21483  hmeoopn  21509  hmeocld  21510  ptuncnv  21550  fbunfip  21613  fgss2  21618  ufilb  21650  ufprim  21653  trufil  21654  cfinufil  21672  ufildr  21675  elfm2  21692  elfm3  21694  rnelfm  21697  fmfnfmlem4  21701  fmco  21705  flimtopon  21714  flimopn  21719  fbflim2  21721  flimrest  21727  flffbas  21739  cnpflf  21745  fclstopon  21756  fclsnei  21763  fclsbas  21765  fclsfnflim  21771  fclscmp  21774  ufilcmp  21776  isfcf  21778  fcfnei  21779  cnpfcf  21785  alexsubb  21790  alexsubALT  21795  cldsubg  21854  tgphaus  21860  tgpt0  21862  tsmsgsum  21882  tsmsres  21887  xbln0  22159  blssexps  22171  blssex  22172  isxms2  22193  prdsbl  22236  neibl  22246  metss  22253  met2ndc  22268  metrest  22269  metcnp3  22285  tngngp3  22400  nmoeq0  22480  xrsxmet  22552  reconn  22571  iccpnfcnv  22683  fgcfil  23009  iscau4  23017  cfilres  23034  iunmbl2  23265  ismbf3d  23361  mbfaddlem  23367  i1faddlem  23400  i1fmullem  23401  ellimc3  23583  tdeglem4  23758  deg1nn0clb  23788  deg1lt0  23789  dvdsq1p  23858  plypf1  23906  0dgrb  23940  plymul0or  23974  ulmshft  24082  ulmcaulem  24086  ulmcau  24087  cosord  24216  eff1olem  24232  lognegb  24274  eflogeq  24286  logdivlt  24305  efopn  24338  cxpeq0  24358  cxpeq  24432  angpieqvd  24492  dcubic  24507  asinsinb  24558  acoscosb  24559  atantanb  24585  rlimcnp  24626  isppw  24774  isppw2  24775  vmappw  24776  isnsqf  24795  ppieq0  24836  fsumdvdsdiag  24844  dvdsppwf1o  24846  fsumfldivdiag  24850  chpeq0  24867  chteq0  24868  dchrptlem1  24923  lgsdir2lem4  24987  lgsne0  24994  lgsqr  25010  lgsdchrval  25013  gausslemma2dlem1a  25024  lgsquadlem1  25039  m1lgs  25047  iscgrglt  25343  brbtwn  25713  brcgr  25714  brbtwn2  25719  axcontlem7  25784  uhgr0vb  25897  ausgrusgrb  25987  ushgredgedg  26048  ushgredgedgloop  26050  usgr0vb  26056  usgr1v  26075  nbupgr  26161  nbumgrvtx  26163  nbuhgr2vtx1edgb  26169  edgusgrnbfin  26196  nb3grprlem1  26203  nbusgrvtxm1uvtx  26227  uvtxnbvtxm1  26228  cusgrfilem2  26273  uhgr0edg0rgrb  26374  cusgrm1rusgr  26382  spthonepeq  26551  usgr2pth  26563  wlkiswwlks  26665  wlkiswwlkupgr  26667  wlklnwwlkn  26673  wlklnwwlknupgr  26675  wwlksnextbi  26692  wwlksnredwwlkn0  26694  wwlksnextwrd  26695  wwlksnextprop  26710  wwlksnwwlksnon  26713  elwwlks2ons3  26751  umgrwwlks2on  26753  elwspths2on  26755  usgr2wspthons3  26759  elwwlks2  26762  elwspths2spth  26763  clwlkclwwlklem3  26803  clwwlksnun  26874  umgr3v3e3cycl  26944  eupth2lem3lem4  26991  frgr0v  27025  frgr3vlem2  27036  frgrncvvdeqlem3  27063  fusgr2wsp2nb  27090  grpoinvf  27274  nvmul0or  27393  nvz  27412  diporthcom  27459  ubthlem3  27616  hvmul0or  27770  his6  27844  hial0  27847  hial02  27848  orthcom  27853  normgt0  27872  ocin  28043  occon3  28044  shsel3  28062  shlub  28161  chssoc  28243  h1de2bi  28301  spansncol  28315  elspansn4  28320  spansnss2  28322  sumspansn  28396  lnopcnbd  28783  lnfncnbd  28804  riesz1  28812  elpjrn  28937  cvcon3  29031  dmdmd  29047  dmdbr3  29052  dmdbr4  29053  dmdbr5  29055  mdslmd1i  29076  atcveq0  29095  chcv1  29102  atssma  29125  atcv0eq  29126  atcv1  29127  bian1d  29194  disjeq1f  29273  br8d  29306  fpwrelmap  29392  xaddeq0  29402  eliccelico  29424  elicoelioo  29425  isarchiofld  29644  unitdivcld  29771  xrge0iifcnv  29803  lmxrge0  29822  indf1ofs  29911  eulerpartlemgh  30263  dstfrvunirn  30359  bnj145OLD  30556  cvmliftmolem2  31025  cvmlift2lem12  31057  mthmb  31239  climuzcnv  31326  br8  31407  br6  31408  br4  31409  funbreq  31425  fprb  31426  axext4dist  31460  nodenselem8  31604  dfrdg4  31753  cgrcom  31792  cgrcoml  31798  cgrdegen  31806  btwncom  31816  brsegle  31910  brsegle2  31911  colinbtwnle  31920  btwnoutside  31927  broutsideof3  31928  outsidele  31934  lineunray  31949  lineelsb2  31950  elhf2  31977  elicc3  32006  nn0prpwlem  32012  opnbnd  32015  cldbnd  32016  opnregcld  32020  cldregopn  32021  fnessref  32047  refssfne  32048  neibastop2  32051  fnemeet2  32057  fnejoin2  32059  fgmin  32060  ontgval  32125  ordtop  32130  ordcmp  32141  nndivsub  32151  bj-ssbbi  32317  bj-ssbft  32337  bj-cbv2hv  32426  bj-dral1v  32444  bj-sbftv  32459  bj-equsal1t  32505  bj-19.21t  32513  bj-ceqsalt0  32573  bj-ceqsalt1  32574  bj-xpnzexb  32648  bj-finsumval0  32819  bj-ldiv  32827  bj-bary1  32834  isbasisrelowllem1  32874  isbasisrelowllem2  32875  finxpsuclem  32905  wl-lem-exsb  33019  wl-mo3t  33029  wl-ax11-lem1  33033  wl-clelv2-just  33050  matunitlindf  33078  poimirlem6  33086  poimirlem7  33087  poimirlem16  33096  poimirlem19  33099  poimirlem22  33102  poimirlem23  33103  poimirlem24  33104  cnambfre  33129  itg2addnc  33135  brabg2  33181  istotbnd3  33241  sstotbnd2  33244  sstotbnd  33245  sstotbnd3  33246  ssbnd  33258  ismtybnd  33277  reheibor  33309  grpoeqdivid  33351  grpokerinj  33363  rngosn3  33394  rngoueqz  33410  1idl  33496  0rngo  33497  divrngidl  33498  igenval2  33536  ispridlc  33540  isdmn3  33544  prtlem10  33669  prter2  33685  dral1-o  33708  lshpinN  33795  lsatcveq0  33838  lsatcv0eq  33853  lsatcv1  33854  islshpcv  33859  lkr0f  33900  lkrshp4  33914  lshpkrlem1  33916  lshpset2N  33925  lfl1dim  33927  lfl1dim2N  33928  lub0N  33995  glb0N  33999  oplecon3b  34006  cmtcomN  34055  cmtbr3N  34060  cmtbr4N  34061  cvrnbtwn2  34081  cvrnbtwn3  34082  cvrcon3b  34083  cvrnbtwn4  34085  cvrcmp  34089  atcvreq0  34120  atnle  34123  atlatle  34126  cvlexchb1  34136  cvlcvr1  34145  hlrelat2  34208  exatleN  34209  cvrval3  34218  cvrval4N  34219  cvrexch  34225  atcvr0eq  34231  lnnat  34232  atcvrj0  34233  atcvrj2b  34237  atltcvr  34240  atbtwn  34251  ps-1  34282  3at  34295  islln2a  34322  llncmp  34327  islpln2a  34353  lplncmp  34367  islvol2aN  34397  4at  34418  lvolcmp  34422  pmaple  34566  lncmp  34588  paddss  34650  llnexchb2lem  34673  2polcon4bN  34723  ispsubcl2N  34752  lhpat3  34851  lautcvr  34897  ltrnid  34940  trlval2  34969  trlatn0  34978  ltrnideq  34981  trlnidatb  34983  cdlemeg49lebilem  35346  trlord  35376  cdlemg1a  35377  cdlemg1cex  35395  tendoid0  35632  dva1dim  35792  cdlemm10N  35926  diarnN  35937  cdlemn  36020  dihlspsnssN  36140  dihatexv  36146  dochkrshp  36194  dochkrshp4  36197  djhlsmcl  36222  lcfl6  36308  lcfl8  36310  lcfrvalsnN  36349  lcfrlem9  36358  mapdval2N  36438  mapdordlem2  36445  mapd1o  36456  mapd0  36473  mapdheq2biN  36538  elrfi  36776  diophrw  36841  eldioph2b  36845  diophin  36855  rexrabdioph  36877  rmxycomplete  37001  coprmdvdsb  37071  jm2.19  37079  jm2.26  37088  jm2.27  37094  limsuc2  37130  dgraa0p  37239  rngunsnply  37263  fiuneneq  37295  pwelg  37385  nzss  38037  dvconstbi  38054  expgrowth  38055  bcc0  38060  axc11next  38128  pm14.24  38154  sbiota1  38156  sbcim2g  38269  sineq0ALT  38695  pwssfi  38733  elixpconstg  38788  mapsnd  38897  mapss2  38906  fsneq  38907  fsneqrn  38912  mapssbi  38914  ssmapsn  38917  rnmptbd2lem  38974  infnsuprnmpt  38976  rnmptbdlem  38981  xralrple2  39069  infxrunb2  39083  xralrple4  39088  xralrple3  39089  xrralrecnnle  39101  xrralrecnnge  39112  reclt0  39113  supxrunb3  39122  supxrleubrnmpt  39131  xrre4  39137  unb2ltle  39141  rexabslelem  39144  suprleubrnmpt  39148  infxrunb3rnmpt  39154  uzub  39157  iccintsng  39195  sqrlearg  39226  uzinico  39233  preimaiocmnf  39234  limcresiooub  39310  limclr  39323  climeldmeq  39333  limsuppnflem  39378  limsupmnflem  39388  limsupmnfuzlem  39394  limsupre3lem  39400  limsupre3uzlem  39403  dvnmul  39495  dvmptfprodlem  39496  ismbl3  39540  ismbl4  39547  fourierdlem50  39710  fourierdlem89  39749  fourierdlem91  39751  dfsalgen2  39896  sge0repnf  39940  sge0lefi  39952  sge0resplit  39960  sge0fodjrnlem  39970  voliunsge0lem  40026  hspdifhsp  40167  isvonmbl  40189  ovnovollem3  40209  vonvolmbl  40212  preimagelt  40249  preimalegt  40250  pimrecltpos  40256  preimaicomnf  40259  pimrecltneg  40270  issmflem  40273  issmfle  40291  issmfgt  40302  smfaddlem1  40308  issmfge  40315  smfresal  40332  smflimmpt  40353  smfinflem  40360  smflimsuplem7  40369  smflimsupmpt  40372  sigarcol  40387  confun  40440  rexsb  40502  2reu2  40521  ralbinrald  40533  rlimdmafv  40591  el1fzopredsuc  40662  2ffzoeq  40665  iccpartiun  40698  ccats1pfxeqbi  40760  reuccatpfxs1  40763  dfodd6  40879  dfeven4  40880  evensumeven  40945  sgoldbalt  40994  sprsymrelfolem2  41061  isassintop  41164  uzlidlring  41247  rngciso  41300  rngcisoALTV  41312  ringciso  41351  ringcisoALTV  41375  domnmsuppn0  41468  lindslininds  41571  snlindsntor  41578  isldepslvec2  41592
  Copyright terms: Public domain W3C validator