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

Theorem impbid 183
Description: Deduce an equivalence from two implications. (Contributed by NM, 5-Aug-1993.) (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 182 . 2  |-  ( ph  ->  ( ph  ->  ( ps 
<->  ch ) ) )
43pm2.43i 43 1  |-  ( ph  ->  ( ps  <->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  bicom1  190  impbid1  194  impcon4bid  196  pm5.74  235  imbi1d  308  pm5.501  330  2falsed  340  impbida  805  dedlem0b  919  dedlema  920  dedlemb  921  albi  1554  exbi  1571  equequ1  1667  equequ1OLD  1668  elequ1  1699  elequ2  1701  19.21t  1802  19.23t  1808  sbequ12  1872  dral1  1918  cbv2h  1933  ax11b  1948  sbft  1978  sbied  1989  sbequ  2013  sb56  2050  sbal1  2078  exsb  2082  dral1-o  2106  eupickb  2221  eupickbi  2222  2eu2  2237  ceqsalt  2823  ceqex  2911  mob2  2958  reu6  2967  sbciegft  3034  eqsbc3r  3061  csbiebt  3130  sseq1  3212  reupick  3465  reupick2  3467  uneqdifeq  3555  disjeq2  4013  disjeq1  4016  disjxiun  4036  disjss3  4038  copsexg  4268  euotd  4283  poeq2  4334  sotric  4356  sotrieq  4357  freq2  4380  seeq1  4381  seeq2  4382  tz7.7  4434  ordtri1  4441  ordtri3  4444  ordelinel  4507  reusv2lem2  4552  reusv2lem3  4553  alxfr  4563  ralxfrd  4564  oneqmin  4612  ordsuc  4621  ordelsuc  4627  ordsucelsuc  4629  ordunisuc2  4651  limsuc  4656  iss  5014  iotaval  5246  funeq  5290  funssres  5310  tz6.12c  5563  fnbrfvb  5579  ssimaex  5600  fvimacnv  5656  elpreima  5661  fsn  5712  fconst2g  5744  fconst5  5747  elunirnALT  5795  f1ocnvfvb  5811  foeqcnvco  5820  f1eqcocnv  5821  fliftfun  5827  soisores  5840  isofr  5855  isose  5856  isopo  5859  isoso  5861  f1oiso2  5865  oprabid  5898  f1opw2  6087  op1steq  6180  rntpos  6263  eusvobj2  6353  smoiso2  6402  seqomlem2  6479  oaord  6561  oawordex  6571  oaordex  6572  omord2  6581  om00  6589  oeord  6602  nnaord  6633  nnmord  6646  nnawordex  6651  nnaordex  6652  erexb  6701  swoord1  6705  swoord2  6706  iiner  6747  eceqoveq  6779  omxpenlem  6979  domtriord  7023  mapxpen  7043  mapunen  7046  ssenen  7051  nneneq  7060  onomeneq  7066  nndomo  7070  fodomfib  7152  f1opwfi  7175  elfiun  7199  suplub2  7228  ordiso2  7246  ordiso  7247  oieu  7270  brwdom2  7303  brwdom3  7312  cantnfreslem  7393  cantnflem1  7407  cardidm  7608  carddom2  7626  pm54.43  7649  pr2ne  7651  acnen  7696  acnen2  7698  alephord  7718  alephinit  7738  dfac5  7771  infdif2  7852  fictb  7887  coflim  7903  fincssdom  7965  fin23lem25  7966  isf32lem9  8003  isf34lem4  8019  fin1a2lem11  8052  axdc3lem2  8093  ficard  8203  fpwwe2lem12  8279  fpwwe2  8281  indpi  8547  nqereq  8575  1idpr  8669  ltapr  8685  leltne  8927  ltlen  8938  ltadd2  8940  ltord1  9315  mul0or  9424  ltmul1  9622  lt2msq  9656  nnsub  9800  nn0sub  10030  zrevaddcl  10079  zltp1le  10083  zdiv  10098  nneo  10111  zeo2  10114  zmax  10329  zbtwnre  10330  qrevaddcl  10354  xrlttri  10489  xrleltne  10495  xralrple  10548  xltneg  10560  xleadd1  10591  xlemul1  10626  supxrunb1  10654  supxrunb2  10655  ioo0  10697  iccid  10717  ico0  10718  ioc0  10719  icc0  10720  difreicc  10783  iccsplit  10784  0fz1  10829  uzsplit  10871  fzm1  10878  fzrevral  10882  flge  10953  modid2  11010  seqf1olem1  11101  hashen  11362  hashdom  11377  shftlem  11579  shftuz  11580  abslt  11814  absle  11815  rexico  11853  cau3lem  11854  rlim2lt  11987  rlim3  11988  o1lo1  12027  rlimdm  12041  climshft  12066  o1dif  12119  isercolllem2  12155  isercoll  12157  zsum  12207  fsum  12209  fsum00  12272  incexclem  12311  dvdsval2  12550  moddvds  12554  negdvdsb  12561  dvdsnegb  12562  dvdscmulr  12573  dvdsmulcr  12574  dvdssub2  12582  fzo0dvdseq  12597  bitsf1ocnv  12651  sadcaddlem  12664  bitsuz  12681  dvdsgcdb  12739  gcdeq  12747  dvdssqlem  12754  isprm2lem  12781  dvdsprime  12787  dvdsprm  12794  coprm  12795  euclemma  12803  rpexp  12815  prmdiveq  12870  odzdvds  12876  pythagtrip  12903  pc2dvds  12947  pcprmpw2  12950  pcprmpw  12951  vdwapun  13037  ramtcl2  13074  firest  13353  mrieqv2d  13557  isacs2  13571  isssc  13713  setciso  13939  posasymb  14102  pleval2  14115  pltval3  14117  lubid  14132  joinle  14143  meetle  14150  lubun  14243  clatleglb  14246  latdisd  14309  letsr  14365  gsumval2a  14475  frmdss2  14501  isgrpid2  14534  isgrpinv  14548  oddvdsnn0  14875  oddvds  14878  odeq  14881  odeq1  14889  gexdvds  14911  pgpfi  14932  pgpssslw  14941  fislw  14952  sylow3lem2  14955  lsmelvalm  14978  lsmlub  14990  lsmss1b  14992  lsmss2b  14994  efgs1b  15061  cyggenod  15187  cyggexb  15201  dprdfeq0  15273  unitmulclb  15463  dvreq1  15491  drngmul0or  15549  isabvd  15601  issrngd  15642  lssats2  15773  lspsneq0  15785  lsmelval2  15854  lvecvs0or  15877  lspsneq  15891  lspsneu  15892  lidl1el  15986  lidldvgen  16023  isnzr2  16031  rrgeq0  16047  domneq0  16054  znunit  16533  ipeq0  16558  ocvsscon  16591  pjdm2  16627  obselocv  16644  unitg  16721  tgss3  16740  clsval2  16803  isopn3  16819  elcls3  16836  opncldf1  16837  neiint  16857  neips  16866  opnneissb  16867  opnssneib  16868  opnnei  16873  tpnei  16874  opnneiid  16879  restcld  16919  restopnb  16922  tgcn  16998  tgcnp  16999  subbascn  17000  cnpnei  17009  cncls2  17018  cncls  17019  cnntr  17020  lmss  17042  hausnei2  17097  lpcls  17108  ordtt1  17123  cmpsub  17143  tgcmp  17144  1stcelcls  17203  kgencn2  17268  ptpjpre1  17282  upxp  17333  txcn  17336  txlm  17358  tgqtop  17419  kqfvima  17437  isr0  17444  regr1lem2  17447  hmeoopn  17473  hmeocld  17474  ptuncnv  17514  fbunfip  17580  fgss2  17585  ufilb  17617  ufprim  17620  trufil  17621  cfinufil  17639  ufildr  17642  elfm2  17659  elfm3  17661  rnelfm  17664  fmfnfmlem4  17668  fmco  17672  flimtopon  17681  flimopn  17686  fbflim2  17688  flimrest  17694  flffbas  17706  cnpflf  17712  fclstopon  17723  fclsnei  17730  fclsbas  17732  fclsfnflim  17738  fclscmp  17741  ufilcmp  17743  isfcf  17745  fcfnei  17746  cnpfcf  17752  alexsubb  17756  alexsubALT  17761  cldsubg  17809  tgphaus  17815  tgpt0  17817  tsmsgsum  17837  tsmsres  17842  xbln0  17981  blssex  17989  isxms2  18010  prdsbl  18053  neibl  18063  metss  18070  met2ndc  18085  metrest  18086  metcnp3  18102  nmoeq0  18261  xrsxmet  18331  reconn  18349  iccpnfcnv  18458  fgcfil  18713  iscau4  18721  cfilres  18738  iunmbl2  18930  ismbf3d  19025  mbfaddlem  19031  i1faddlem  19064  i1fmullem  19065  ellimc3  19245  tdeglem4  19462  deg1nn0clb  19492  deg1lt0  19493  dvdsq1p  19562  plypf1  19610  0dgrb  19644  plymul0or  19677  ulmshft  19785  ulmcaulem  19787  ulmcau  19788  cosord  19910  eff1olem  19926  lognegb  19959  eflogeq  19971  logdivlt  19988  efopn  20021  cxpeq0  20041  cxpeq  20113  angpieqvd  20144  dcubic  20158  asinsinb  20209  acoscosb  20210  atantanb  20236  rlimcnp  20276  isppw  20368  isppw2  20369  vmappw  20370  isnsqf  20389  ppieq0  20430  fsumdvdsdiag  20440  dvdsppwf1o  20442  fsumfldivdiag  20446  chpeq0  20463  chteq0  20464  dchrptlem1  20519  lgsdir2lem4  20581  lgsne0  20588  lgsqr  20601  lgsdchrval  20602  lgsquadlem1  20609  m1lgs  20617  grpoinvf  20923  rngosn3  21109  rngosn4  21110  rngoueqz  21113  nvmul0or  21226  nvz  21251  diporthcom  21308  ubthlem3  21467  hvmul0or  21620  his6  21694  hial0  21697  hial02  21698  orthcom  21703  normgt0  21722  ocin  21891  occon3  21892  shsel3  21910  shlub  22009  chssoc  22091  h1de2bi  22149  spansncol  22163  elspansn4  22168  spansnss2  22170  sumspansn  22244  lnopcnbd  22632  lnfncnbd  22653  riesz1  22661  elpjrn  22786  cvcon3  22880  dmdmd  22896  dmdbr3  22901  dmdbr4  22902  dmdbr5  22904  mdslmd1i  22925  atcveq0  22944  chcv1  22951  atssma  22974  atcv0eq  22975  atcv1  22976  funimass4f  23058  ballotlemsf1o  23088  eliccioo  23131  bisimpd  23136  bian1d  23138  eliccelico  23285  elicoelioo  23286  unitdivcld  23300  xaddeq0  23319  xrsinvgval  23321  xrge0iifcnv  23330  disjabrex  23374  disjabrexf  23375  lmxrge0  23390  imambfm  23582  indf1ofs  23624  orvcgteel  23683  orvclteel  23688  dstfrvunirn  23690  cvmliftmolem2  23828  cvmlift2lem12  23860  eupath2lem3  23918  ghomf1olem  24016  climuzcnv  24019  relexpindlem  24051  mulge0b  24101  zprod  24160  fprod  24164  br8  24184  br6  24185  br4  24186  funbreq  24198  fprb  24200  axext4dist  24228  nodenselem8  24413  dfrdg4  24560  brbtwn  24599  brcgr  24600  brbtwn2  24605  axcontlem7  24670  cgrcom  24685  cgrcoml  24691  cgrdegen  24699  btwncom  24709  brsegle  24803  brsegle2  24804  colinbtwnle  24813  btwnoutside  24820  broutsideof3  24821  outsidele  24827  lineunray  24842  lineelsb2  24843  elhf2  24877  ontgval  24942  ordtop  24947  ordcmp  24958  nndivsub  24968  wl-bibi1  24985  itg2addnc  25005  copsexgb  25069  boxbid  25114  nxtbid  25115  diabid  25116  untbi12d  25125  domrngref  25163  domintreflemb  25165  f1ofi  25173  twsymr  25181  injrec2  25222  surjsec2  25223  repcpwti  25264  cbicp  25269  dupre1  25346  inposet  25381  dffprod  25422  grpodivfo  25477  trran2  25496  ltrran2  25506  rltrran  25517  rngoridfz  25540  svli2  25587  svs2  25590  cldifemp  25627  iscnp4  25666  limptlimpr  25679  flfnei2  25680  iint  25715  trran  25717  dmrngcmp  25854  ismonc  25917  isepic  25927  sgplpte21e  26240  xsyysx  26248  pdiveql  26271  abhp  26276  elicc3  26331  nn0prpwlem  26341  opnbnd  26346  cldbnd  26347  opnregcld  26351  cldregopn  26352  fnessref  26396  refssfne  26397  locfincmp  26407  neibastop2  26413  fnemeet2  26419  fnejoin2  26421  fgmin  26422  brabg2  26469  istotbnd3  26598  sstotbnd2  26601  sstotbnd  26602  sstotbnd3  26603  ssbnd  26615  ismtybnd  26634  reheibor  26666  grpoeqdivid  26674  grpokerinj  26678  1idl  26754  0rngo  26755  divrngidl  26756  igenval2  26794  ispridlc  26798  isdmn3  26802  prtlem10  26836  prter2  26852  ralxpmap  26864  elrfi  26872  diophrw  26941  eldioph2b  26945  diophin  26955  rexrabdioph  26978  rmxycomplete  27105  coprmdvdsb  27177  jm2.19  27189  jm2.26  27198  jm2.27  27204  limsuc2  27240  islinds4  27408  dgraa0p  27457  rngunsnply  27481  fiuneneq  27616  hashgcdlem  27619  dvconstbi  27654  expgrowth  27655  ax10ext  27709  pm14.24  27735  sbiota1  27737  sigarcol  27957  rexsb  28049  2reu2  28068  ralbinrald  28080  rlimdmafv  28145  hashtpg  28217  nbusgra  28277  nb3graprlem1  28287  nbcusgra  28298  uvtxnbgra  28306  3v3e3cycl  28411  frgra3vlem2  28425  sbcim2g  28601  bnj145  29071  dral1NEW7  29470  cbv2hwAUX7  29490  sbiedNEW7  29515  sbftNEW7  29531  sbequNEW7  29554  sb56NEW7  29568  exsbNEW7  29571  sbal1NEW7  29587  ax11bNEW7  29594  cbv2hOLD7  29675  ax9lem2  29763  lubunNEW  29785  lshpinN  29801  lsatcveq0  29844  lsatcv0eq  29859  lsatcv1  29860  islshpcv  29865  lkr0f  29906  lkrshp4  29920  lshpkrlem1  29922  lshpset2N  29931  lfl1dim  29933  lfl1dim2N  29934  lub0N  30001  glb0N  30005  oplecon3b  30012  cmtcomN  30061  cmtbr3N  30066  cmtbr4N  30067  cvrnbtwn2  30087  cvrnbtwn3  30088  cvrcon3b  30089  cvrnbtwn4  30091  cvrcmp  30095  atcvreq0  30126  atnle  30129  atlatle  30132  cvlexchb1  30142  cvlcvr1  30151  hlrelat2  30214  exatleN  30215  cvrval3  30224  cvrval4N  30225  cvrexch  30231  atcvr0eq  30237  lnnat  30238  atcvrj0  30239  atcvrj2b  30243  atltcvr  30246  atbtwn  30257  ps-1  30288  3at  30301  islln2a  30328  llncmp  30333  islpln2a  30359  lplncmp  30373  islvol2aN  30403  4at  30424  lvolcmp  30428  pmaple  30572  lncmp  30594  paddss  30656  llnexchb2lem  30679  2polcon4bN  30729  ispsubcl2N  30758  lhpat3  30857  lautcvr  30903  ltrnid  30946  trlval2  30974  trlatn0  30983  ltrnideq  30986  trlnidatb  30988  cdlemeg49lebilem  31350  trlord  31380  cdlemg1a  31381  cdlemg1cex  31399  tendoid0  31636  dva1dim  31796  cdlemm10N  31930  diarnN  31941  cdlemn  32024  dihlspsnssN  32144  dihatexv  32150  dochkrshp  32198  dochkrshp4  32201  djhlsmcl  32226  lcfl6  32312  lcfl8  32314  lcfrvalsnN  32353  lcfrlem9  32362  mapdval2N  32442  mapdordlem2  32449  mapd1o  32460  mapd0  32477  mapdheq2biN  32542
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator