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

Theorem impbid 203
Description: Deduce an equivalence from two implications. Deduction associated with impbi 199 and impbii 200. (Contributed by NM, 24-Jan-1993.) Revised to prove it from impbid21d 202. (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 202 . 2 (𝜑 → (𝜑 → (𝜓𝜒)))
43pm2.43i 52 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197
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 198
This theorem is referenced by:  bicom1  212  impbid1  216  impcon4bid  218  pm5.74  261  imbi1d  332  pm5.501  357  2falsed  367  impbida  826  dedlem0b  1058  dedlema  1059  dedlemb  1060  albi  1903  alexbii  1917  equequ1  2122  equequ2  2123  elequ1  2164  elequ2  2171  19.21tOLDOLD  2242  sbequ12  2280  sb56  2284  19.21tOLD  2389  cbv2h  2444  dral1  2489  dral1ALT  2490  ax12b  2505  sbequ  2537  sbft  2540  exsb  2631  eupickb  2713  eupickbi  2714  2eu2  2729  ceqsalt  3433  rspcebdv  3518  ceqex  3538  mob2  3595  reu6  3604  sbciegft  3675  csbiebt  3759  sseq1  3834  ssdifsym  4076  reupick  4123  reupick2  4125  uneqdifeq  4264  prnebg  4587  preqsnd  4590  prel12g  4597  disjeq2  4827  disjeq1  4830  disjss3  4854  reusv2lem2  5081  reusv2lem3  5082  alxfr  5089  ralxfrd  5090  ralxfrd2  5094  copsexg  5158  snopeqop  5173  euotd  5181  poeq2  5249  sotric  5271  sotrieq  5272  freq2  5295  seeq1  5296  seeq2  5297  iss  5665  tz7.7  5975  ordtri1  5982  ordelinel  6048  iotaval  6084  funeq  6130  funssres  6153  f0dom0  6313  tz6.12c  6442  fnbrfvb  6465  ssimaex  6493  fvimacnv  6563  elpreima  6568  eldmrexrnb  6597  fsn  6634  fnsnb  6666  fmptsng  6668  fmptsnd  6669  tpres  6700  fconst2g  6702  fconst5  6705  elunirn  6742  f1ocnvfvb  6768  foeqcnvco  6788  f1eqcocnv  6789  fliftfun  6795  soisores  6810  isofr  6825  isose  6826  isopo  6829  isoso  6831  f1oiso2  6835  eusvobj2  6876  oprabid  6914  f1opw2  7127  oneqmin  7244  ordsuc  7253  ordelsuc  7259  ordsucelsuc  7261  ordunisuc2  7283  limsuc  7288  f1ovv  7376  op1steq  7451  fvn0elsuppb  7555  extmptsuppeq  7562  rntpos  7609  smoiso2  7711  seqomlem2  7791  oaord  7873  oawordex  7883  oaordex  7884  omord2  7893  om00  7901  oeord  7914  nnaord  7945  nnmord  7958  nnawordex  7963  nnaordex  7964  erexb  8013  swoord1  8019  swoord2  8020  iiner  8063  eceqoveq  8097  mapsnd  8143  ralxpmap  8153  omxpenlem  8309  domtriord  8354  mapxpen  8374  mapunen  8377  ssenen  8382  nneneq  8391  onomeneq  8398  nndomo  8402  en1eqsnbi  8439  fodomfib  8488  f1opwfi  8518  fsuppunbi  8544  elfiun  8584  suplub2  8615  ordiso2  8668  ordiso  8669  oieu  8692  brwdom2  8726  brwdom3  8735  cantnflem1  8842  cardidm  9077  carddom2  9095  pm54.43  9118  pr2ne  9120  acnen  9168  acnen2  9170  alephord  9190  alephinit  9210  dfac5  9243  infdif2  9326  fictb  9361  coflim  9377  fincssdom  9439  fin23lem25  9440  isf32lem9  9477  isf34lem4  9493  fin1a2lem11  9526  axdc3lem2  9567  ficard  9681  fpwwe2lem12  9757  fpwwe2  9759  indpi  10023  nqereq  10051  1idpr  10145  ltapr  10161  leltne  10421  ltlen  10432  ltadd2  10435  addlsub  10741  addid0  10744  ltord1  10848  mul0or  10961  ltmul1  11167  mulge0b  11187  lt2msq  11202  negfi  11265  nnsub  11356  nn0sub  11628  zrevaddcl  11707  zltp1le  11712  zdiv  11732  nneo  11746  zeo2  11749  zmax  12023  zbtwnre  12024  qrevaddcl  12048  xrlttri  12207  xrleltne  12213  xralrple  12273  xltneg  12285  xleadd1  12322  xlemul1  12357  supxrunb1  12386  supxrunb2  12387  ioo0  12437  iccid  12457  ico0  12458  ioc0  12459  icc0  12460  difreicc  12546  iccsplit  12547  zltaddlt1le  12566  0fz1  12603  uzsplit  12654  fzm1  12662  fzrevral  12667  ssfzo12bi  12806  elfznelfzob  12817  flge  12849  modid2  12940  modmuladd  12955  ssnn0fi  13027  seqf1olem1  13082  hashen  13374  hashdom  13405  hash2exprb  13489  pr2pwpr  13497  hashtpg  13503  len0nnbi  13571  reuccats1  13723  ccats1swrdeqbi  13741  repsdf2  13768  scshwfzeqfzo  13815  relexpindlem  14045  shftlem  14050  shftuz  14051  abslt  14296  absle  14297  rexico  14335  cau3lem  14336  rlim2lt  14470  rlim3  14471  o1lo1  14510  rlimdm  14524  climshft  14549  o1dif  14602  isercolllem2  14638  isercoll  14640  zsum  14691  fsum  14693  fsum00  14771  incexclem  14809  zprod  14907  fprod  14911  dvdsval2  15225  moddvds  15233  negdvdsb  15240  dvdsnegb  15241  dvdscmulr  15252  dvdsmulcr  15253  dvdssub2  15265  dvdsaddre2b  15271  fzo0dvdseq  15287  mod2eq1n2dvds  15310  ltoddhalfle  15324  sumodd  15350  bitsf1ocnv  15404  sadcaddlem  15417  bitsuz  15434  dvdsgcdb  15500  gcdzeq  15509  dvdssqlem  15517  lcmeq0  15551  lcmdvdsb  15564  lcmfeq0b  15581  lcmf  15584  lcmfdvdsb  15594  coprmgcdb  15600  cncongr  15620  isprm2lem  15631  dvdsprime  15637  dvdsprm  15651  isprm7  15656  coprm  15659  euclemma  15661  rpexp  15668  prmdiveq  15727  hashgcdlem  15729  odzdvds  15736  pythagtrip  15775  pc2dvds  15819  pcprmpw2  15822  pcprmpw  15823  vdwapun  15914  ramtcl2  15951  firest  16317  mrieqv2d  16523  isacs2  16537  isssc  16703  setciso  16964  posasymb  17176  pleval2  17189  pltval3  17191  lublecllem  17212  joinle  17238  meetle  17252  lubun  17347  clatleglb  17350  latdisd  17414  letsr  17451  intopsn  17477  gsumval2a  17503  frmdss2  17624  isgrpid2  17682  isgrpinv  17696  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  18642  ringinvnz1ne0  18813  ringinvnzdiv  18814  unitmulclb  18886  dvreq1  18914  f1rhm0to0  18963  f1rhm0to0ALT  18964  drngmul0or  18991  isabvd  19043  issrngd  19084  lssats2  19226  lspsneq0  19238  lsmelval2  19311  lvecvs0or  19334  lspsneq  19348  lspsneu  19349  lidl1el  19446  lidldvgen  19483  isnzr2  19491  0ringnnzr  19497  0ring01eqbi  19501  rrgeq0  19518  domneq0  19525  ply1coe1eq  19895  cply1coe0bi  19897  znunit  20138  psgndif  20175  ipeq0  20212  ocvsscon  20249  pjdm2  20285  obselocv  20302  islinds4  20404  mat1dimelbas  20508  cramer  20730  toponcomb  20967  tgss3  21024  clsval2  21088  isopn3  21104  elcls3  21121  opncldf1  21122  neiint  21142  neips  21151  opnneissb  21152  opnssneib  21153  opnnei  21158  tpnei  21159  opnneiid  21164  restcld  21210  restopnb  21213  tgcn  21290  tgcnp  21291  subbascn  21292  iscnp4  21301  cnpnei  21302  cncls2  21311  cncls  21312  cnntr  21313  lmss  21336  hausnei2  21391  lpcls  21402  ordtt1  21417  cmpsub  21437  tgcmp  21438  1stcelcls  21498  locfincmp  21563  kgencn2  21594  ptpjpre1  21608  upxp  21660  txcn  21663  txlm  21685  tgqtop  21749  kqfvima  21767  isr0  21774  regr1lem2  21777  hmeoopn  21803  hmeocld  21804  ptuncnv  21844  fbunfip  21906  fgss2  21911  ufilb  21943  ufprim  21946  trufil  21947  cfinufil  21965  ufildr  21968  elfm2  21985  elfm3  21987  rnelfm  21990  fmfnfmlem4  21994  fmco  21998  flimtopon  22007  flimopn  22012  fbflim2  22014  flimrest  22020  flffbas  22032  cnpflf  22038  fclstopon  22049  fclsnei  22056  fclsbas  22058  fclsfnflim  22064  fclscmp  22067  ufilcmp  22069  isfcf  22071  fcfnei  22072  cnpfcf  22078  alexsubb  22083  alexsubALT  22088  cldsubg  22147  tgphaus  22153  tgpt0  22155  tsmsgsum  22175  tsmsres  22180  xbln0  22452  blssexps  22464  blssex  22465  isxms2  22486  prdsbl  22529  neibl  22539  metss  22546  met2ndc  22561  metrest  22562  metcnp3  22578  tngngp3  22693  nmoeq0  22773  xrsxmet  22845  reconn  22864  iccpnfcnv  22976  fgcfil  23302  iscau4  23310  cfilres  23327  iunmbl2  23560  ismbf3d  23657  mbfaddlem  23663  i1faddlem  23696  i1fmullem  23697  ellimc3  23879  tdeglem4  24056  deg1nn0clb  24086  deg1lt0  24087  dvdsq1p  24156  plypf1  24204  0dgrb  24238  plymul0or  24272  ulmshft  24380  ulmcaulem  24384  ulmcau  24385  cosord  24515  eff1olem  24531  lognegb  24572  eflogeq  24584  logdivlt  24603  efopn  24640  cxpeq0  24660  cxpeq  24734  angpieqvd  24794  dcubic  24809  asinsinb  24860  acoscosb  24861  atantanb  24887  rlimcnp  24928  isppw  25076  isppw2  25077  vmappw  25078  isnsqf  25097  ppieq0  25138  fsumdvdsdiag  25146  dvdsppwf1o  25148  fsumfldivdiag  25152  chpeq0  25169  chteq0  25170  dchrptlem1  25225  lgsdir2lem4  25289  lgsne0  25296  lgsqr  25312  lgsdchrval  25315  gausslemma2dlem1a  25326  lgsquadlem1  25341  m1lgs  25349  iscgrglt  25645  brbtwn  26015  brcgr  26016  brbtwn2  26021  axcontlem7  26086  uhgr0vb  26203  edglnl  26275  ausgrusgrb  26297  ushgredgedg  26358  ushgredgedgloop  26360  ushgredgedgloopOLD  26361  usgr0vb  26367  usgr1v  26386  nbupgr  26478  nbumgrvtx  26480  nbuhgr2vtx1edgb  26486  edgusgrnbfin  26513  nb3grprlem1  26520  uvtxnbvtxm1  26551  cusgrfilem2  26602  uhgr0edg0rgrb  26720  cusgrm1rusgr  26728  spthonepeq  26898  usgr2pth  26910  wlkiswwlks  27025  wlkiswwlkupgr  27027  wlklnwwlkn  27033  wlklnwwlknupgr  27035  wwlksnextbi  27053  wwlksnredwwlkn0  27055  wwlksnextwrd  27056  wwlksnextprop  27072  wwlksnwwlksnonOLD  27077  elwwlks2ons3OLD  27118  umgrwwlks2on  27120  elwspths2on  27123  usgr2wspthons3  27128  elwwlks2  27130  elwspths2spth  27131  clwlkclwwlklem3  27166  loopclwwlkn1b  27213  clwwlknon1sn  27290  clwwlknonwwlknonb  27296  clwwlknonwwlknonbOLD  27297  clwwlknunOLD  27308  umgr3v3e3cycl  27379  eupth2lem3lem4  27426  frgr0v  27458  frgr3vlem2  27471  2clwwlk2clwwlk  27549  wlkl0  27569  grpoinvf  27737  nvmul0or  27855  nvz  27874  diporthcom  27921  ubthlem3  28078  hvmul0or  28232  his6  28306  hial0  28309  hial02  28310  orthcom  28315  normgt0  28334  ocin  28505  occon3  28506  shsel3  28524  shlub  28623  chssoc  28705  h1de2bi  28763  spansncol  28777  elspansn4  28782  spansnss2  28784  sumspansn  28858  lnopcnbd  29245  lnfncnbd  29266  riesz1  29274  elpjrn  29399  cvcon3  29493  dmdmd  29509  dmdbr3  29514  dmdbr4  29515  dmdbr5  29517  mdslmd1i  29538  atcveq0  29557  chcv1  29564  atssma  29587  atcv0eq  29588  atcv1  29589  bian1d  29656  disjeq1f  29734  br8d  29769  fpwrelmap  29857  xaddeq0  29867  eliccelico  29888  elicoelioo  29889  isarchiofld  30164  unitdivcld  30294  xrge0iifcnv  30326  lmxrge0  30345  indf1ofs  30435  eulerpartlemgh  30787  dstfrvunirn  30883  cvmliftmolem2  31608  cvmlift2lem12  31640  mthmb  31822  climuzcnv  31908  br8  31989  br6  31990  br4  31991  funbreq  32011  fprb  32012  axext4dist  32047  nodenselem8  32183  dfrdg4  32400  cgrcom  32439  cgrcoml  32445  cgrdegen  32453  btwncom  32463  brsegle  32557  brsegle2  32558  colinbtwnle  32567  btwnoutside  32574  broutsideof3  32575  outsidele  32581  lineunray  32596  lineelsb2  32597  elhf2  32624  elicc3  32653  nn0prpwlem  32659  opnbnd  32662  cldbnd  32663  opnregcld  32667  cldregopn  32668  fnessref  32694  refssfne  32695  neibastop2  32698  fnemeet2  32704  fnejoin2  32706  fgmin  32707  ontgval  32768  ordtop  32773  ordcmp  32784  nndivsub  32794  bj-ssbbi  32959  bj-ssbft  32978  bj-cbv2hv  33066  bj-dral1v  33083  bj-sbftv  33097  bj-equsal1t  33140  bj-19.21t  33148  bj-ceqsalt0  33199  bj-ceqsalt1  33200  bj-xpnzexb  33276  bj-finsumval0  33482  bj-ldiv  33490  bj-bary1  33497  dfgcd3  33505  isbasisrelowllem1  33537  isbasisrelowllem2  33538  finxpsuclem  33568  wl-lem-exsb  33680  wl-mo3t  33690  wl-ax11-lem1  33694  wl-clelv2-just  33710  matunitlindf  33738  poimirlem6  33746  poimirlem7  33747  poimirlem16  33756  poimirlem19  33759  poimirlem22  33762  poimirlem23  33763  poimirlem24  33764  cnambfre  33788  itg2addnc  33794  brabg2  33840  istotbnd3  33899  sstotbnd2  33902  sstotbnd  33903  sstotbnd3  33904  ssbnd  33916  ismtybnd  33935  reheibor  33967  grpoeqdivid  34009  grpokerinj  34021  rngosn3  34052  rngoueqz  34068  1idl  34154  0rngo  34155  divrngidl  34156  igenval2  34194  ispridlc  34198  isdmn3  34202  relcnveq3  34425  iss2  34443  elrelscnveq3  34572  prtlem10  34662  prter2  34678  dral1-o  34701  lshpinN  34787  lsatcveq0  34830  lsatcv0eq  34845  lsatcv1  34846  islshpcv  34851  lkr0f  34892  lkrshp4  34906  lshpkrlem1  34908  lshpset2N  34917  lfl1dim  34919  lfl1dim2N  34920  lub0N  34987  glb0N  34991  oplecon3b  34998  cmtcomN  35047  cmtbr3N  35052  cmtbr4N  35053  cvrnbtwn2  35073  cvrnbtwn3  35074  cvrcon3b  35075  cvrnbtwn4  35077  cvrcmp  35081  atcvreq0  35112  atnle  35115  atlatle  35118  cvlexchb1  35128  cvlcvr1  35137  hlrelat2  35201  exatleN  35202  cvrval3  35211  cvrval4N  35212  cvrexch  35218  atcvr0eq  35224  lnnat  35225  atcvrj0  35226  atcvrj2b  35230  atltcvr  35233  atbtwn  35244  ps-1  35275  3at  35288  islln2a  35315  llncmp  35320  islpln2a  35346  lplncmp  35360  islvol2aN  35390  4at  35411  lvolcmp  35415  pmaple  35559  lncmp  35581  paddss  35643  llnexchb2lem  35666  2polcon4bN  35716  ispsubcl2N  35745  lhpat3  35844  lautcvr  35890  ltrnid  35933  trlval2  35961  trlatn0  35970  ltrnideq  35973  trlnidatb  35975  cdlemeg49lebilem  36337  trlord  36367  cdlemg1a  36368  cdlemg1cex  36386  tendoid0  36623  dva1dim  36783  cdlemm10N  36916  diarnN  36927  cdlemn  37010  dihlspsnssN  37130  dihatexv  37136  dochkrshp  37184  dochkrshp4  37187  djhlsmcl  37212  lcfl6  37298  lcfl8  37300  lcfrvalsnN  37339  lcfrlem9  37348  mapdval2N  37428  mapdordlem2  37435  mapd1o  37446  mapd0  37463  mapdheq2biN  37528  elrfi  37776  diophrw  37841  eldioph2b  37845  diophin  37855  rexrabdioph  37877  rmxycomplete  38000  coprmdvdsb  38070  jm2.19  38078  jm2.26  38087  jm2.27  38093  limsuc2  38129  dgraa0p  38237  rngunsnply  38261  fiuneneq  38293  pwelg  38382  nzss  39033  dvconstbi  39050  expgrowth  39051  bcc0  39056  axc11next  39123  pm14.24  39149  sbiota1  39151  sbcim2g  39263  sineq0ALT  39684  pwssfi  39721  elixpconstg  39776  mapss2  39901  fsneq  39902  fsneqrn  39907  mapssbi  39909  ssmapsn  39912  rnmptbd2lem  39963  infnsuprnmpt  39965  rnmptbdlem  39970  xralrple2  40067  infxrunb2  40081  xralrple4  40086  xralrple3  40087  xrralrecnnle  40099  xrralrecnnge  40109  reclt0  40110  supxrunb3  40119  supxrleubrnmpt  40128  xrre4  40134  unb2ltle  40138  rexabslelem  40141  suprleubrnmpt  40145  infxrunb3rnmpt  40151  uzub  40154  supminfrnmpt  40168  iccintsng  40247  sqrlearg  40277  uzinico  40284  preimaiocmnf  40285  limcresiooub  40371  limclr  40384  climeldmeq  40394  limsuppnflem  40439  limsupmnflem  40449  limsupmnfuzlem  40455  limsupre3lem  40461  limsupre3uzlem  40464  liminfreuzlem  40531  dvnmul  40655  dvmptfprodlem  40656  ismbl3  40699  ismbl4  40706  fourierdlem50  40869  fourierdlem89  40908  fourierdlem91  40910  dfsalgen2  41055  sge0repnf  41099  sge0lefi  41111  sge0resplit  41119  sge0fodjrnlem  41129  voliunsge0lem  41185  hspdifhsp  41329  isvonmbl  41351  ovnovollem3  41371  vonvolmbl  41374  preimagelt  41411  preimalegt  41412  pimrecltpos  41418  preimaicomnf  41421  pimrecltneg  41432  issmflem  41435  issmfle  41453  issmfgt  41464  smfaddlem1  41470  issmfge  41477  smfresal  41494  smflimmpt  41515  smfinflem  41522  smflimsuplem7  41531  smflimsupmpt  41534  sigarcol  41552  confun  41605  rexsb  41698  2reu2  41716  ralbinrald  41728  rlimdmafv  41783  fafv2elrnb  41841  tz6.12c-afv2  41848  dfatbrafv2b  41851  fnbrafv2b  41854  rlimdmafv2  41864  f1oresf1o2  41898  el1fzopredsuc  41927  2ffzoeq  41930  iccpartiun  41962  ccats1pfxeqbi  42023  reuccatpfxs1  42026  dfodd6  42142  dfeven4  42143  evensumeven  42208  sbgoldbalt  42261  sprsymrelfolem2  42328  isassintop  42431  uzlidlring  42514  rngciso  42567  rngcisoALTV  42579  ringciso  42618  ringcisoALTV  42642  domnmsuppn0  42735  lindslininds  42838  snlindsntor  42845  isldepslvec2  42859
  Copyright terms: Public domain W3C validator