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

Theorem impbid 215
Description: Deduce an equivalence from two implications. Deduction associated with impbi 211 and impbii 212. (Contributed by NM, 24-Jan-1993.) Revised to prove it from impbid21d 214. (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 214 . 2 (𝜑 → (𝜑 → (𝜓𝜒)))
43pm2.43i 52 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209
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 210
This theorem is referenced by:  bicom1  224  impbid1  228  impcon4bid  230  pm5.74  273  imbi1d  345  pm5.501  370  2falsedOLD  381  impbida  800  dedlem0b  1040  dedlema  1041  dedlemb  1042  albi  1820  alexbii  1834  equequ1  2033  equequ2  2034  spsbbi  2079  sbbidvOLD  2086  sbequOLD  2093  elequ1  2122  elequ2  2130  sbbidOLD  2250  sbequ12  2255  sbft  2272  sb56OLD  2280  sbequvvOLD  2337  cbv2w  2359  exsb  2380  dral1v  2389  cbv2  2425  cbv2h  2428  ax12b  2448  dral1  2463  dral1ALT  2464  sbequ12ALT  2583  sbftALT  2595  sbequALT  2599  eupickb  2723  eupickbi  2724  2eu2  2740  ralbi  3162  ceqsalt  3513  vtoclgft  3539  rspcebdv  3603  ceqex  3631  mob2  3692  reu6  3703  sbciegft  3794  2reu2  3865  csbiebt  3895  sseq1  3978  ssdifsym  4225  reupick  4272  reupick2  4274  uneqdifeq  4421  prnebg  4770  preqsnd  4773  prel12g  4778  iuneqconst  4916  disjeq2  5022  disjeq1  5025  disjss3  5052  reusv2lem2  5288  reusv2lem3  5289  alxfr  5296  ralxfrd  5297  ralxfrd2  5301  copsexgw  5369  copsexg  5370  snopeqop  5384  euotd  5391  poeq2  5466  sotric  5489  sotrieq  5490  freq2  5514  seeq1  5515  seeq2  5516  iss  5892  tz7.7  6206  ordtri1  6213  ordelinel  6278  iotaval  6319  funeq  6365  funssres  6388  f0dom0  6555  tz6.12c  6688  fnbrfvb  6711  ssimaex  6741  fvimacnv  6816  elpreima  6821  eldmrexrnb  6851  fsn  6890  fnsnb  6921  fmptsng  6923  fmptsnd  6924  fprb  6949  tpres  6956  fconst2g  6958  fconst5  6961  elunirn  7004  f1ocnvfvb  7030  f1prex  7034  foeqcnvco  7050  f1eqcocnv  7051  f1eqcocnvOLD  7052  fliftfun  7060  soisores  7075  isofr  7090  isose  7091  isopo  7094  isoso  7096  f1oiso2  7100  eusvobj2  7144  oprabidw  7182  oprabid  7183  f1opw2  7396  oneqmin  7516  ordsuc  7525  ordelsuc  7531  ordsucelsuc  7533  ordunisuc2  7555  limsuc  7560  f1ovv  7656  op1steq  7730  opreuopreu  7731  funeldmdif  7744  fvn0elsuppb  7845  extmptsuppeq  7852  rntpos  7903  smoiso2  8004  seqomlem2  8085  oaord  8171  oawordex  8181  oaordex  8182  omord2  8191  om00  8199  oeord  8212  nnaord  8243  nnmord  8256  nnawordex  8261  nnaordex  8262  erexb  8312  swoord1  8318  swoord2  8319  iiner  8367  eceqoveq  8400  mapsnd  8448  ralxpmap  8458  omxpenlem  8616  domtriord  8662  mapxpen  8682  mapunen  8685  ssenen  8690  nneneq  8699  nndomog  8707  onomeneq  8708  en1eqsnbi  8748  fodomfib  8797  f1opwfi  8827  fsuppunbi  8853  elfiun  8893  suplub2  8924  ordiso2  8978  ordiso  8979  oieu  9002  brwdom2  9036  brwdom3  9045  cantnflem1  9151  cardidm  9387  carddom2  9405  pm54.43  9429  pr2ne  9431  acnen  9479  acnen2  9481  alephord  9501  alephinit  9521  dfac5  9554  infdif2  9632  fictb  9667  coflim  9683  fincssdom  9745  fin23lem25  9746  isf32lem9  9783  isf34lem4  9799  fin1a2lem11  9832  axdc3lem2  9873  ficard  9987  fpwwe2lem12  10063  fpwwe2  10065  indpi  10329  nqereq  10357  1idpr  10451  ltapr  10467  leltne  10730  ltlen  10741  ltadd2  10744  addlsub  11056  addid0  11059  ltord1  11166  mul0or  11280  ldiv  11474  ltmul1  11490  mulge0b  11510  lt2msq  11525  negfi  11588  nnsub  11680  nn0sub  11946  zrevaddcl  12026  zltp1le  12031  zdiv  12051  nneo  12065  zeo2  12068  zmax  12344  zbtwnre  12345  qrevaddcl  12369  xrlttri  12531  xrleltne  12537  xralrple  12597  xltneg  12609  xleadd1  12647  xlemul1  12682  supxrunb1  12711  supxrunb2  12712  ioo0  12762  iccid  12782  ico0  12783  ioc0  12784  icc0  12785  difreicc  12873  iccsplit  12874  zltaddlt1le  12894  0fz1  12933  uzsplit  12985  fzm1  12993  fzrevral  12998  ssfzo12bi  13138  elfznelfzob  13149  flge  13181  modid2  13272  modmuladd  13287  ssnn0fi  13359  seqf1olem1  13416  hashen  13714  hashdom  13747  hash2exprb  13836  pr2pwpr  13844  hashtpg  13850  len0nnbi  13905  ccats1pfxeqbi  14106  reuccatpfxs1  14111  repsdf2  14142  scshwfzeqfzo  14190  relexpindlem  14424  shftlem  14429  shftuz  14430  abslt  14676  absle  14677  rexico  14715  cau3lem  14716  reusq0  14824  rlim2lt  14856  rlim3  14857  o1lo1  14896  rlimdm  14910  climshft  14935  o1dif  14988  isercolllem2  15024  isercoll  15026  zsum  15077  fsum  15079  fsum00  15155  incexclem  15193  zprod  15293  fprod  15297  dvdsval2  15612  moddvds  15620  negdvdsb  15628  dvdsnegb  15629  dvdscmulr  15640  dvdsmulcr  15641  dvdssub2  15653  dvdsaddre2b  15659  fzo0dvdseq  15675  mod2eq1n2dvds  15698  ltoddhalfle  15712  sumodd  15739  bitsf1ocnv  15793  sadcaddlem  15806  bitsuz  15823  dvdsgcdb  15893  gcdzeq  15902  dvdssqlem  15910  lcmeq0  15944  lcmdvdsb  15957  lcmfeq0b  15974  lcmf  15977  lcmfdvdsb  15987  coprmgcdb  15993  cncongr  16013  isprm2lem  16025  dvdsprime  16031  dvdsprm  16047  isprm7  16052  coprm  16055  euclemma  16057  rpexp  16064  prmdiveq  16123  hashgcdlem  16125  odzdvds  16132  pythagtrip  16171  pc2dvds  16215  pcprmpw2  16218  pcprmpw  16219  vdwapun  16310  ramtcl2  16347  firest  16708  mrieqv2d  16912  isacs2  16926  isssc  17092  setciso  17353  posasymb  17564  pleval2  17577  pltval3  17579  lublecllem  17600  joinle  17626  meetle  17640  lubun  17735  clatleglb  17738  latdisd  17802  letsr  17839  intopsn  17866  gsumval2a  17897  frmdss2  18030  isgrpid2  18142  isgrpinv  18158  symg1bas  18521  oddvdsnn0  18674  oddvds  18677  odeq  18680  odeq1  18689  gexdvds  18711  pgpfi  18732  pgpssslw  18741  fislw  18752  sylow3lem2  18755  lsmelvalm  18778  lsmlub  18792  lsmss1b  18794  lsmss2b  18796  efgs1b  18864  cyggenod  19005  cyggexb  19021  dprdfeq0  19146  ablsimpgfind  19234  ringinvnz1ne0  19347  ringinvnzdiv  19348  unitmulclb  19420  dvreq1  19448  f1ghm0to0  19497  f1rhm0to0ALT  19498  drngmul0or  19525  isabvd  19593  issrngd  19634  lssats2  19774  lspsneq0  19786  lsmelval2  19859  lvecvs0or  19882  lspsneq  19896  lspsneu  19897  lidl1el  19993  lidldvgen  20030  isnzr2  20038  0ringnnzr  20044  0ring01eqbi  20048  rrgeq0  20065  domneq0  20072  znunit  20264  psgndif  20300  ipeq0  20336  ocvsscon  20373  pjdm2  20409  obselocv  20426  islinds4  20533  ply1coe1eq  20936  cply1coe0bi  20938  mat1dimelbas  21085  cramer  21305  toponcomb  21543  tgss3  21600  clsval2  21664  isopn3  21680  elcls3  21697  opncldf1  21698  neiint  21718  neips  21727  opnneissb  21728  opnssneib  21729  opnnei  21734  tpnei  21735  opnneiid  21740  restcld  21786  restopnb  21789  tgcn  21866  tgcnp  21867  subbascn  21868  iscnp4  21877  cnpnei  21878  cncls2  21887  cncls  21888  cnntr  21889  lmss  21912  hausnei2  21967  lpcls  21978  ordtt1  21993  cmpsub  22014  tgcmp  22015  1stcelcls  22075  locfincmp  22140  kgencn2  22171  ptpjpre1  22185  upxp  22237  txcn  22240  txlm  22262  tgqtop  22326  kqfvima  22344  isr0  22351  regr1lem2  22354  hmeoopn  22380  hmeocld  22381  ptuncnv  22421  fbunfip  22483  fgss2  22488  ufilb  22520  ufprim  22523  trufil  22524  cfinufil  22542  ufildr  22545  elfm2  22562  elfm3  22564  rnelfm  22567  fmfnfmlem4  22571  fmco  22575  flimtopon  22584  flimopn  22589  fbflim2  22591  flimrest  22597  flffbas  22609  cnpflf  22615  fclstopon  22626  fclsnei  22633  fclsbas  22635  fclsfnflim  22641  fclscmp  22644  ufilcmp  22646  isfcf  22648  fcfnei  22649  cnpfcf  22655  alexsubb  22660  alexsubALT  22665  cldsubg  22725  tgphaus  22731  tgpt0  22733  tsmsgsum  22753  tsmsres  22758  xbln0  23030  blssexps  23042  blssex  23043  isxms2  23064  prdsbl  23107  neibl  23117  metss  23124  met2ndc  23139  metrest  23140  metcnp3  23156  tngngp3  23271  nmoeq0  23351  xrsxmet  23423  reconn  23442  iccpnfcnv  23558  fgcfil  23884  iscau4  23892  cfilres  23909  iunmbl2  24170  ismbf3d  24267  mbfaddlem  24273  i1faddlem  24306  i1fmullem  24307  ellimc3  24491  tdeglem4  24670  deg1nn0clb  24700  deg1lt0  24701  dvdsq1p  24770  plypf1  24818  0dgrb  24852  plymul0or  24886  ulmshft  24994  ulmcaulem  24998  ulmcau  24999  cosord  25132  eff1olem  25149  lognegb  25190  eflogeq  25202  logdivlt  25221  efopn  25258  cxpeq0  25278  cxpeq  25355  angpieqvd  25426  dcubic  25441  asinsinb  25492  acoscosb  25493  atantanb  25519  rlimcnp  25560  isppw  25708  isppw2  25709  vmappw  25710  isnsqf  25729  ppieq0  25770  fsumdvdsdiag  25778  dvdsppwf1o  25780  fsumfldivdiag  25784  chpeq0  25801  chteq0  25802  dchrptlem1  25857  lgsdir2lem4  25921  lgsne0  25928  lgsqr  25944  lgsdchrval  25947  gausslemma2dlem1a  25958  lgsquadlem1  25973  m1lgs  25981  2sqreultblem  26041  2sqreunnltblem  26044  iscgrglt  26317  brbtwn  26702  brcgr  26703  brbtwn2  26708  axcontlem7  26773  uhgr0vb  26874  edglnl  26945  ausgrusgrb  26967  ushgredgedg  27028  ushgredgedgloop  27030  usgr0vb  27036  usgr1v  27055  nbupgr  27143  nbumgrvtx  27145  nbuhgr2vtx1edgb  27151  edgusgrnbfin  27172  nb3grprlem1  27179  uvtxnbvtxm1  27205  cusgrfilem2  27255  uhgr0edg0rgrb  27373  cusgrm1rusgr  27381  spthonepeq  27550  usgr2pth  27562  wlkiswwlks  27671  wlkiswwlkupgr  27673  wlklnwwlkn  27679  wlklnwwlknupgr  27681  wwlksnextbi  27689  wwlksnredwwlkn0  27691  wwlksnextwrd  27692  wwlksnextprop  27707  umgrwwlks2on  27752  elwspths2on  27755  usgr2wspthons3  27759  elwwlks2  27761  elwspths2spth  27762  clwlkclwwlklem3  27795  loopclwwlkn1b  27836  clwwlknon1sn  27894  clwwlknonwwlknonb  27900  umgr3v3e3cycl  27978  eupth2lem3lem4  28025  frgr0v  28056  frgr3vlem2  28068  2clwwlk2clwwlk  28144  wlkl0  28161  grpoinvf  28324  nvmul0or  28442  nvz  28461  diporthcom  28508  ubthlem3  28664  hvmul0or  28817  his6  28891  hial0  28894  hial02  28895  orthcom  28900  normgt0  28919  ocin  29088  occon3  29089  shsel3  29107  shlub  29206  chssoc  29288  h1de2bi  29346  spansncol  29360  elspansn4  29365  spansnss2  29367  sumspansn  29441  lnopcnbd  29828  lnfncnbd  29849  riesz1  29857  elpjrn  29982  cvcon3  30076  dmdmd  30092  dmdbr3  30097  dmdbr4  30098  dmdbr5  30100  mdslmd1i  30121  atcveq0  30140  chcv1  30147  atssma  30170  atcv0eq  30171  atcv1  30172  bian1d  30239  disjeq1f  30342  br8d  30380  fpwrelmap  30490  xaddeq0  30498  eliccelico  30521  elicoelioo  30522  isarchiofld  30933  unitdivcld  31229  xrge0iifcnv  31261  lmxrge0  31280  indf1ofs  31370  eulerpartlemgh  31721  dstfrvunirn  31817  loop1cycl  32469  cusgracyclt3v  32488  cvmliftmolem2  32614  cvmlift2lem12  32646  satfvsucsuc  32697  satfdm  32701  fmlasuc  32718  satffunlem1lem2  32735  satffunlem2lem2  32738  mthmb  32913  climuzcnv  32999  br8  33077  br6  33078  br4  33079  funbreq  33098  axextbdist  33130  nodenselem8  33280  dfrdg4  33497  cgrcom  33536  cgrcoml  33542  cgrdegen  33550  btwncom  33560  brsegle  33654  brsegle2  33655  colinbtwnle  33664  btwnoutside  33671  broutsideof3  33672  outsidele  33678  lineunray  33693  lineelsb2  33694  elhf2  33721  elicc3  33750  nn0prpwlem  33755  opnbnd  33758  cldbnd  33759  opnregcld  33763  cldregopn  33764  fnessref  33790  refssfne  33791  neibastop2  33794  fnemeet2  33800  fnejoin2  33802  fgmin  33803  ontgval  33864  ordtop  33869  ordcmp  33880  nndivsub  33890  bj-19.21t  34185  bj-19.23t  34186  bj-19.42t  34189  bj-sbft  34191  bj-cbv2hv  34206  bj-equsal1t  34232  bj-19.21t0  34240  bj-ceqsalt0  34296  bj-ceqsalt1  34297  bj-xpnzexb  34369  bj-idreseq  34549  bj-imdiridlem  34572  bj-finsumval0  34672  bj-fvimacnv0  34673  bj-isrvec2  34686  bj-bary1  34698  dfgcd3  34710  isbasisrelowllem1  34744  isbasisrelowllem2  34745  finxpsuclem  34786  wl-lem-exsb  34939  wl-mo3t  34949  wl-ax11-lem1  34954  matunitlindf  35027  poimirlem6  35035  poimirlem7  35036  poimirlem16  35045  poimirlem19  35048  poimirlem22  35051  poimirlem23  35052  poimirlem24  35053  cnambfre  35077  itg2addnc  35083  brabg2  35126  istotbnd3  35181  sstotbnd2  35184  sstotbnd  35185  sstotbnd3  35186  ssbnd  35198  ismtybnd  35217  reheibor  35249  grpoeqdivid  35291  grpokerinj  35303  rngosn3  35334  rngoueqz  35350  1idl  35436  0rngo  35437  divrngidl  35438  igenval2  35476  ispridlc  35480  isdmn3  35484  relcnveq3  35710  iss2  35733  elrelscnveq3  35863  funALTVeq  36065  disjeq  36099  prtlem10  36133  prter2  36149  dral1-o  36172  lshpinN  36257  lsatcveq0  36300  lsatcv0eq  36315  lsatcv1  36316  islshpcv  36321  lkr0f  36362  lkrshp4  36376  lshpkrlem1  36378  lshpset2N  36387  lfl1dim  36389  lfl1dim2N  36390  lub0N  36457  glb0N  36461  oplecon3b  36468  cmtcomN  36517  cmtbr3N  36522  cmtbr4N  36523  cvrnbtwn2  36543  cvrnbtwn3  36544  cvrcon3b  36545  cvrnbtwn4  36547  cvrcmp  36551  atcvreq0  36582  atnle  36585  atlatle  36588  cvlexchb1  36598  cvlcvr1  36607  hlrelat2  36671  exatleN  36672  cvrval3  36681  cvrval4N  36682  cvrexch  36688  atcvr0eq  36694  lnnat  36695  atcvrj0  36696  atcvrj2b  36700  atltcvr  36703  atbtwn  36714  ps-1  36745  3at  36758  islln2a  36785  llncmp  36790  islpln2a  36816  lplncmp  36830  islvol2aN  36860  4at  36881  lvolcmp  36885  pmaple  37029  lncmp  37051  paddss  37113  llnexchb2lem  37136  2polcon4bN  37186  ispsubcl2N  37215  lhpat3  37314  lautcvr  37360  ltrnid  37403  trlval2  37431  trlatn0  37440  ltrnideq  37443  trlnidatb  37445  cdlemeg49lebilem  37807  trlord  37837  cdlemg1a  37838  cdlemg1cex  37856  tendoid0  38093  dva1dim  38253  cdlemm10N  38386  diarnN  38397  cdlemn  38480  dihlspsnssN  38600  dihatexv  38606  dochkrshp  38654  dochkrshp4  38657  djhlsmcl  38682  lcfl6  38768  lcfl8  38770  lcfrvalsnN  38809  lcfrlem9  38818  mapdval2N  38898  mapdordlem2  38905  mapd1o  38916  mapd0  38933  mapdheq2biN  38998  nnproddivdvdsd  39264  fnsnbt  39375  frlmfzowrdb  39398  frlmsnic  39414  prjspreln0  39547  elrfi  39579  diophrw  39644  eldioph2b  39648  diophin  39657  rexrabdioph  39679  rmxycomplete  39802  coprmdvdsb  39870  jm2.19  39878  jm2.26  39887  jm2.27  39893  limsuc2  39929  dgraa0p  40037  rngunsnply  40061  fiuneneq  40085  pwelg  40203  nzss  40969  dvconstbi  40986  expgrowth  40987  bcc0  40992  axc11next  41058  pm14.24  41084  sbiota1  41086  sbcim2g  41192  sineq0ALT  41591  pwssfi  41627  mapss2  41786  fsneq  41787  fsneqrn  41792  mapssbi  41794  ssmapsn  41797  rnmptbd2lem  41838  infnsuprnmpt  41840  rnmptbdlem  41845  xralrple2  41939  infxrunb2  41953  xralrple4  41958  xralrple3  41959  xrralrecnnle  41970  xrralrecnnge  41979  reclt0  41980  supxrunb3  41989  supxrleubrnmpt  41996  xrre4  42001  unb2ltle  42005  rexabslelem  42008  suprleubrnmpt  42012  infxrunb3rnmpt  42018  uzub  42021  supminfrnmpt  42035  iccintsng  42113  sqrlearg  42143  uzinico  42150  preimaiocmnf  42151  limcresiooub  42237  limclr  42250  climeldmeq  42260  limsuppnflem  42305  limsupmnflem  42315  limsupmnfuzlem  42321  limsupre3lem  42327  limsupre3uzlem  42330  liminfreuzlem  42397  dvnmul  42538  dvmptfprodlem  42539  ismbl3  42581  ismbl4  42588  fourierdlem50  42751  fourierdlem89  42790  fourierdlem91  42792  dfsalgen2  42934  sge0repnf  42978  sge0lefi  42990  sge0resplit  42998  sge0fodjrnlem  43008  voliunsge0lem  43064  hspdifhsp  43208  isvonmbl  43230  ovnovollem3  43250  vonvolmbl  43253  pimrecltpos  43297  preimaicomnf  43300  pimrecltneg  43311  issmflem  43314  issmfle  43332  issmfgt  43343  smfaddlem1  43349  issmfge  43356  smfresal  43373  smflimmpt  43394  smfinflem  43401  smflimsuplem7  43410  smflimsupmpt  43413  sigarcol  43431  confun  43485  or2expropbi  43579  rexsb  43607  euoreqb  43618  ralbinrald  43631  rlimdmafv  43686  fafv2elrnb  43744  tz6.12c-afv2  43751  dfatbrafv2b  43754  fnbrafv2b  43757  rlimdmafv2  43767  f1oresf1o2  43800  el1fzopredsuc  43835  2ffzoeq  43838  imasetpreimafvbijlemfo  43875  iccpartiun  43904  ichnfb  43935  ich2exprop  43941  sprsymrelfolem2  43963  paireqne  43981  prprelprb  43987  reupr  43992  requad01  44092  requad1  44093  requad2  44094  dfodd6  44108  dfeven4  44109  evensumeven  44178  sbgoldbalt  44252  isomushgr  44297  isomuspgr  44305  isomgrsymb  44308  isassintop  44423  uzlidlring  44506  rngciso  44559  rngcisoALTV  44571  ringciso  44610  ringcisoALTV  44634  domnmsuppn0  44724  lindslininds  44826  snlindsntor  44833  isldepslvec2  44847  affinecomb1  45069  prelrrx2b  45081  rrx2plord2  45089  eenglngeehlnm  45106  rrx2vlinest  45108  line2xlem  45120  line2x  45121  line2y  45122  itsclc0xyqsolb  45137  itsclquadb  45143
  Copyright terms: Public domain W3C validator