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

Theorem impbid 191
Description: Deduce an equivalence from two implications. (Contributed by NM, 24-Jan-1993.) Revised to prove it from impbid21d 190. (Revised by Wolf Lammen, 3-Nov-2012.)
Hypotheses
Ref Expression
impbid.1  |-  ( ph  ->  ( ps  ->  ch ) )
impbid.2  |-  ( ph  ->  ( ch  ->  ps ) )
Assertion
Ref Expression
impbid  |-  ( ph  ->  ( ps  <->  ch )
)

Proof of Theorem impbid
StepHypRef Expression
1 impbid.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
2 impbid.2 . . 3  |-  ( ph  ->  ( ch  ->  ps ) )
31, 2impbid21d 190 . 2  |-  ( ph  ->  ( ph  ->  ( ps 
<->  ch ) ) )
43pm2.43i 47 1  |-  ( ph  ->  ( ps  <->  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
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 185
This theorem is referenced by:  bicom1  199  impbid1  203  impcon4bid  205  pm5.74  244  imbi1d  317  pm5.501  341  2falsed  351  impbida  832  dedlem0b  953  dedlema  954  dedlemb  955  albi  1626  exbi  1653  equequ1  1784  elequ1  1807  elequ2  1809  19.21t  1890  19.23t  1895  sbequ12  1978  cbv2h  2005  dral1  2053  dral1ALT  2054  ax12b  2072  sbequ  2103  sbft  2106  sb56  2158  exsb  2198  dral1-o  2219  eupickb  2346  eupickbi  2347  2eu2  2364  eleq2d  2513  ceqsalt  3118  ceqex  3216  mob2  3265  reu6  3274  sbciegft  3344  eqsbc3r  3375  csbiebt  3440  sseq1  3510  reupick  3767  reupick2  3769  uneqdifeq  3902  prnebg  4197  disjeq2  4411  disjeq1  4414  disjxiun  4434  disjss3  4436  reusv2lem2  4639  reusv2lem3  4640  alxfr  4650  ralxfrd  4651  copsexg  4722  copsexgOLD  4723  euotd  4738  poeq2  4794  sotric  4816  sotrieq  4817  freq2  4840  seeq1  4841  seeq2  4842  tz7.7  4894  ordtri1  4901  ordtri3  4904  ordelinel  4966  iss  5311  iotaval  5552  funeq  5597  funssres  5618  f0dom0  5759  tz6.12c  5875  fnbrfvb  5898  ssimaex  5923  fvimacnv  5987  elpreima  5992  eldmrexrnb  6023  fsn  6054  fnsnb  6075  fmptsng  6077  fmptsnd  6078  fconst2g  6110  fconst5  6113  elunirn  6148  f1ocnvfvb  6170  foeqcnvco  6188  f1eqcocnv  6189  fliftfun  6195  soisores  6208  isofr  6223  isose  6224  isopo  6227  isoso  6229  f1oiso2  6233  eusvobj2  6274  oprabid  6308  f1opw2  6513  oneqmin  6625  ordsuc  6634  ordelsuc  6640  ordsucelsuc  6642  ordunisuc2  6664  limsuc  6669  f1ovv  6756  op1steq  6827  extmptsuppeq  6926  rntpos  6970  smoiso2  7042  seqomlem2  7118  oaord  7198  oawordex  7208  oaordex  7209  omord2  7218  om00  7226  oeord  7239  nnaord  7270  nnmord  7283  nnawordex  7288  nnaordex  7289  erexb  7338  swoord1  7342  swoord2  7343  iiner  7385  eceqoveq  7418  ralxpmap  7470  omxpenlem  7620  domtriord  7665  mapxpen  7685  mapunen  7688  ssenen  7693  nneneq  7702  onomeneq  7709  nndomo  7713  en1eqsnbi  7752  fodomfib  7802  f1opwfi  7826  fsuppunbi  7852  elfiun  7892  suplub2  7923  ordiso2  7943  ordiso  7944  oieu  7967  brwdom2  8002  brwdom3  8011  cantnflem1  8111  cantnflem1OLD  8134  cardidm  8343  carddom2  8361  pm54.43  8384  pr2ne  8386  acnen  8437  acnen2  8439  alephord  8459  alephinit  8479  dfac5  8512  infdif2  8593  fictb  8628  coflim  8644  fincssdom  8706  fin23lem25  8707  isf32lem9  8744  isf34lem4  8760  fin1a2lem11  8793  axdc3lem2  8834  ficard  8943  fpwwe2lem12  9022  fpwwe2  9024  indpi  9288  nqereq  9316  1idpr  9410  ltapr  9426  leltne  9677  ltlen  9689  ltadd2  9691  ltord1  10086  mul0or  10196  ltmul1  10399  mulge0b  10419  lt2msq  10436  nnsub  10581  nn0sub  10853  zrevaddcl  10916  zltp1le  10920  zdiv  10940  nneo  10953  zeo2  10956  zmax  11190  zbtwnre  11191  qrevaddcl  11215  xrlttri  11356  xrleltne  11362  xralrple  11415  xltneg  11427  xleadd1  11458  xlemul1  11493  supxrunb1  11522  supxrunb2  11523  ioo0  11565  iccid  11585  ico0  11586  ioc0  11587  icc0  11588  difreicc  11663  iccsplit  11664  0fz1  11716  uzsplit  11761  fzm1  11769  fzrevral  11774  ssfzo12bi  11889  elfznelfzob  11898  flge  11924  modid2  12005  ssnn0fi  12076  seqf1olem1  12128  hashen  12402  hashdom  12429  hashle00  12447  hash2prb  12499  pr2pwpr  12502  hashtpg  12505  reuccats1  12688  ccats1swrdeqbi  12705  repsdf2  12732  scshwfzeqfzo  12776  shftlem  12883  shftuz  12884  abslt  13129  absle  13130  rexico  13168  cau3lem  13169  rlim2lt  13302  rlim3  13303  o1lo1  13342  rlimdm  13356  climshft  13381  o1dif  13434  isercolllem2  13470  isercoll  13472  zsum  13522  fsum  13524  fsum00  13594  incexclem  13630  zprod  13726  fprod  13730  dvdsval2  13971  moddvds  13975  negdvdsb  13982  dvdsnegb  13983  dvdscmulr  13994  dvdsmulcr  13995  dvdssub2  14005  fzo0dvdseq  14021  bitsf1ocnv  14076  sadcaddlem  14089  bitsuz  14106  dvdsgcdb  14164  gcdeq  14172  dvdssqlem  14179  isprm2lem  14206  dvdsprime  14212  dvdsprm  14222  coprm  14223  euclemma  14231  rpexp  14243  prmdiveq  14298  odzdvds  14304  pythagtrip  14340  pc2dvds  14384  pcprmpw2  14387  pcprmpw  14388  vdwapun  14474  ramtcl2  14511  firest  14812  mrieqv2d  15018  isacs2  15032  isssc  15171  setciso  15397  posasymb  15561  pleval2  15574  pltval3  15576  lublecllem  15597  joinle  15623  meetle  15637  lubun  15732  clatleglb  15735  latdisd  15799  letsr  15836  intopsn  15861  gsumval2a  15885  frmdss2  16010  isgrpid2  16065  isgrpinv  16079  symg1bas  16400  oddvdsnn0  16547  oddvds  16550  odeq  16553  odeq1  16561  gexdvds  16583  pgpfi  16604  pgpssslw  16613  fislw  16624  sylow3lem2  16627  lsmelvalm  16650  lsmlub  16662  lsmss1b  16664  lsmss2b  16666  efgs1b  16733  cyggenod  16866  cyggexb  16880  dprdfeq0  17041  dprdfeq0OLD  17048  unitmulclb  17293  dvreq1  17321  f1rhm0to0  17368  f1rhm0to0ALT  17369  drngmul0or  17396  isabvd  17448  issrngd  17489  lssats2  17625  lspsneq0  17637  lsmelval2  17710  lvecvs0or  17733  lspsneq  17747  lspsneu  17748  lidl1el  17845  lidldvgen  17882  isnzr2  17890  0ringnnzr  17896  0ring01eqbi  17900  rrgeq0  17917  domneq0  17925  ply1coe1eq  18319  cply1coe0bi  18321  znunit  18580  psgndif  18616  ipeq0  18651  ocvsscon  18684  pjdm2  18720  obselocv  18737  islinds4  18848  mat1dimelbas  18951  cramer  19171  unitgOLD  19447  tgss3  19466  clsval2  19529  isopn3  19545  elcls3  19562  opncldf1  19563  neiint  19583  neips  19592  opnneissb  19593  opnssneib  19594  opnnei  19599  tpnei  19600  opnneiid  19605  restcld  19651  restopnb  19654  tgcn  19731  tgcnp  19732  subbascn  19733  iscnp4  19742  cnpnei  19743  cncls2  19752  cncls  19753  cnntr  19754  lmss  19777  hausnei2  19832  lpcls  19843  ordtt1  19858  cmpsub  19878  tgcmp  19879  1stcelcls  19940  locfincmp  20005  kgencn2  20036  ptpjpre1  20050  upxp  20102  txcn  20105  txlm  20127  tgqtop  20191  kqfvima  20209  isr0  20216  regr1lem2  20219  hmeoopn  20245  hmeocld  20246  ptuncnv  20286  fbunfip  20348  fgss2  20353  ufilb  20385  ufprim  20388  trufil  20389  cfinufil  20407  ufildr  20410  elfm2  20427  elfm3  20429  rnelfm  20432  fmfnfmlem4  20436  fmco  20440  flimtopon  20449  flimopn  20454  fbflim2  20456  flimrest  20462  flffbas  20474  cnpflf  20480  fclstopon  20491  fclsnei  20498  fclsbas  20500  fclsfnflim  20506  fclscmp  20509  ufilcmp  20511  isfcf  20513  fcfnei  20514  cnpfcf  20520  alexsubb  20524  alexsubALT  20529  cldsubg  20587  tgphaus  20593  tgpt0  20595  tsmsgsum  20615  tsmsgsumOLD  20618  tsmsresOLD  20623  tsmsres  20624  xbln0  20895  blssexps  20907  blssex  20908  isxms2  20929  prdsbl  20972  neibl  20982  metss  20989  met2ndc  21004  metrest  21005  metcnp3  21021  nmoeq0  21221  xrsxmet  21292  reconn  21311  iccpnfcnv  21422  fgcfil  21688  iscau4  21696  cfilres  21713  iunmbl2  21945  ismbf3d  22039  mbfaddlem  22045  i1faddlem  22078  i1fmullem  22079  ellimc3  22261  tdeglem4  22436  deg1nn0clb  22468  deg1lt0  22469  dvdsq1p  22539  plypf1  22587  0dgrb  22621  plymul0or  22655  ulmshft  22763  ulmcaulem  22767  ulmcau  22768  cosord  22897  eff1olem  22913  lognegb  22952  eflogeq  22964  logdivlt  22984  efopn  23017  cxpeq0  23037  cxpeq  23109  angpieqvd  23140  dcubic  23155  asinsinb  23206  acoscosb  23207  atantanb  23233  rlimcnp  23273  isppw  23366  isppw2  23367  vmappw  23368  isnsqf  23387  ppieq0  23428  fsumdvdsdiag  23438  dvdsppwf1o  23440  fsumfldivdiag  23444  chpeq0  23461  chteq0  23462  dchrptlem1  23517  lgsdir2lem4  23579  lgsne0  23586  lgsqr  23599  lgsdchrval  23600  lgsquadlem1  23607  m1lgs  23615  brbtwn  24180  brcgr  24181  brbtwn2  24186  axcontlem7  24251  ausisusgra  24333  nbgraf1olem5  24423  edgusgranbfin  24428  nb3graprlem1  24429  cusgrarn  24437  nbcusgra  24441  cusgrafilem2  24458  uvtxnbgra  24471  uvtxnb  24475  spthonepeq  24567  3v3e3cycl  24643  wlkiswwlk  24676  wlklniswwlkn  24679  wwlknextbi  24703  wwlknredwwlkn0  24705  wwlkextwrd  24706  wwlkextprop  24722  0clwlk  24743  clwlkisclwwlklem0  24766  el2wlkonot  24847  el2spthonot  24848  el2wlkonotot0  24850  el2wlksotot  24860  usg2wlkonot  24861  usg2spthonot  24866  usg2spthonot0  24867  nbhashuvtx  24894  uvtxhashnb  24895  0eusgraiff0rgra  24917  cusgraiffrusgra  24918  eupath2lem3  24957  frgra3vlem2  24979  frgrancvvdeqlem3  25010  numclwwlkun  25057  grpoinvf  25220  rngosn3  25406  rngoueqz  25410  rngoridfz  25415  nvmul0or  25525  nvz  25550  diporthcom  25607  ubthlem3  25766  hvmul0or  25920  his6  25994  hial0  25997  hial02  25998  orthcom  26003  normgt0  26022  ocin  26192  occon3  26193  shsel3  26211  shlub  26310  chssoc  26392  h1de2bi  26450  spansncol  26464  elspansn4  26469  spansnss2  26471  sumspansn  26545  lnopcnbd  26933  lnfncnbd  26954  riesz1  26962  elpjrn  27087  cvcon3  27181  dmdmd  27197  dmdbr3  27202  dmdbr4  27203  dmdbr5  27205  mdslmd1i  27226  atcveq0  27245  chcv1  27252  atssma  27275  atcv0eq  27276  atcv1  27277  bian1d  27344  br8d  27441  fpwrelmap  27534  xaddeq0  27551  eliccelico  27566  elicoelioo  27567  isarchiofld  27785  unitdivcld  27861  xrge0iifcnv  27893  lmxrge0  27912  indf1ofs  28017  eulerpartlemgh  28295  dstfrvunirn  28391  cvmliftmolem2  28705  cvmlift2lem12  28737  mthmb  28919  ghomf1olem  29012  climuzcnv  29015  relexpindlem  29040  br8  29161  br6  29162  br4  29163  funbreq  29177  fprb  29179  axext4dist  29209  nodenselem8  29424  dfrdg4  29576  cgrcom  29616  cgrcoml  29622  cgrdegen  29630  btwncom  29640  brsegle  29734  brsegle2  29735  colinbtwnle  29744  btwnoutside  29751  broutsideof3  29752  outsidele  29758  lineunray  29773  lineelsb2  29774  elhf2  29808  ontgval  29872  ordtop  29877  ordcmp  29888  nndivsub  29898  wl-lem-exsb  29991  wl-mo3t  29997  wl-ax11-lem1  30001  cnambfre  30039  itg2addnc  30045  elicc3  30111  nn0prpwlem  30116  opnbnd  30119  cldbnd  30120  opnregcld  30124  cldregopn  30125  fnessref  30151  refssfne  30152  neibastop2  30155  fnemeet2  30161  fnejoin2  30163  fgmin  30164  brabg2  30182  istotbnd3  30243  sstotbnd2  30246  sstotbnd  30247  sstotbnd3  30248  ssbnd  30260  ismtybnd  30279  reheibor  30311  grpoeqdivid  30319  grpokerinj  30323  1idl  30399  0rngo  30400  divrngidl  30401  igenval2  30439  ispridlc  30443  isdmn3  30447  prtlem10  30582  prter2  30598  elrfi  30602  diophrw  30668  eldioph2b  30672  diophin  30682  rexrabdioph  30703  rmxycomplete  30829  coprmdvdsb  30901  jm2.19  30911  jm2.26  30920  jm2.27  30926  limsuc2  30962  dgraa0p  31074  rngunsnply  31098  fiuneneq  31130  hashgcdlem  31133  isprm7  31168  lcmeq0  31182  lcmdvdsb  31193  nzss  31198  dvconstbi  31215  expgrowth  31216  axc11next  31267  pm14.24  31293  sbiota1  31295  iccintsng  31517  limcresiooub  31602  limclr  31615  dvnmul  31694  dvmptfprodlem  31695  fourierdlem50  31893  fourierdlem89  31932  fourierdlem91  31934  sigarcol  32035  rexsb  32127  2reu2  32146  ralbinrald  32158  rlimdmafv  32216  ralxfrd2  32257  2ffzoeq  32295  usgra2pth  32308  uhgrauhgbi  32328  uhg0v  32331  isassintop  32487  tpres  32506  uzlidlring  32562  rngciso  32665  rngcisoOLD  32677  ringciso  32713  ringcisoOLD  32737  domnmsuppn0  32832  lindslininds  32935  snlindsntor  32942  isldepslvec2  32956  sbcim2g  33177  sineq0ALT  33605  bnj145OLD  33650  bj-iftru  34035  bj-iffal  34036  bj-cbv2hv  34177  bj-dral1v  34209  bj-sbftv  34228  bj-sb56  34232  bj-equsal1t  34278  bj-19.21t  34286  bj-ceqsalt0  34332  bj-ceqsalt1  34333  bj-xpnzexb  34401  bj-finsumval0  34538  bj-lsub  34546  bj-ldiv  34549  bj-bary1  34556  lshpinN  34589  lsatcveq0  34632  lsatcv0eq  34647  lsatcv1  34648  islshpcv  34653  lkr0f  34694  lkrshp4  34708  lshpkrlem1  34710  lshpset2N  34719  lfl1dim  34721  lfl1dim2N  34722  lub0N  34789  glb0N  34793  oplecon3b  34800  cmtcomN  34849  cmtbr3N  34854  cmtbr4N  34855  cvrnbtwn2  34875  cvrnbtwn3  34876  cvrcon3b  34877  cvrnbtwn4  34879  cvrcmp  34883  atcvreq0  34914  atnle  34917  atlatle  34920  cvlexchb1  34930  cvlcvr1  34939  hlrelat2  35002  exatleN  35003  cvrval3  35012  cvrval4N  35013  cvrexch  35019  atcvr0eq  35025  lnnat  35026  atcvrj0  35027  atcvrj2b  35031  atltcvr  35034  atbtwn  35045  ps-1  35076  3at  35089  islln2a  35116  llncmp  35121  islpln2a  35147  lplncmp  35161  islvol2aN  35191  4at  35212  lvolcmp  35216  pmaple  35360  lncmp  35382  paddss  35444  llnexchb2lem  35467  2polcon4bN  35517  ispsubcl2N  35546  lhpat3  35645  lautcvr  35691  ltrnid  35734  trlval2  35763  trlatn0  35772  ltrnideq  35775  trlnidatb  35777  cdlemeg49lebilem  36140  trlord  36170  cdlemg1a  36171  cdlemg1cex  36189  tendoid0  36426  dva1dim  36586  cdlemm10N  36720  diarnN  36731  cdlemn  36814  dihlspsnssN  36934  dihatexv  36940  dochkrshp  36988  dochkrshp4  36991  djhlsmcl  37016  lcfl6  37102  lcfl8  37104  lcfrvalsnN  37143  lcfrlem9  37152  mapdval2N  37232  mapdordlem2  37239  mapd1o  37250  mapd0  37267  mapdheq2biN  37332  pwelg  37583
  Copyright terms: Public domain W3C validator