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  1551  exbi  1568  equequ1  1648  elequ1  1687  elequ2  1689  19.21t  1790  19.23t  1796  sbequ12  1860  dral1  1905  cbv2h  1920  ax11b  1935  sbft  1965  sbied  1976  sbequ  2000  sb56  2037  sbal1  2065  exsb  2069  dral1-o  2093  eupickb  2208  eupickbi  2209  2eu2  2224  ceqsalt  2810  ceqex  2898  mob2  2945  reu6  2954  sbciegft  3021  eqsbc3r  3048  csbiebt  3117  sseq1  3199  reupick  3452  reupick2  3454  uneqdifeq  3542  disjeq2  3997  disjeq1  4000  disjxiun  4020  disjss3  4022  copsexg  4252  euotd  4267  poeq2  4318  sotric  4340  sotrieq  4341  freq2  4364  seeq1  4365  seeq2  4366  tz7.7  4418  ordtri1  4425  ordtri3  4428  ordelinel  4491  reusv2lem2  4536  reusv2lem3  4537  alxfr  4547  ralxfrd  4548  oneqmin  4596  ordsuc  4605  ordelsuc  4611  ordsucelsuc  4613  ordunisuc2  4635  limsuc  4640  iss  4998  iotaval  5230  funeq  5274  funssres  5294  tz6.12c  5547  fnbrfvb  5563  ssimaex  5584  fvimacnv  5640  elpreima  5645  fsn  5696  fconst2g  5728  fconst5  5731  elunirnALT  5779  f1ocnvfvb  5795  foeqcnvco  5804  f1eqcocnv  5805  fliftfun  5811  soisores  5824  isofr  5839  isose  5840  isopo  5843  isoso  5845  f1oiso2  5849  oprabid  5882  f1opw2  6071  op1steq  6164  rntpos  6247  eusvobj2  6337  smoiso2  6386  seqomlem2  6463  oaord  6545  oawordex  6555  oaordex  6556  omord2  6565  om00  6573  oeord  6586  nnaord  6617  nnmord  6630  nnawordex  6635  nnaordex  6636  erexb  6685  swoord1  6689  swoord2  6690  iiner  6731  eceqoveq  6763  omxpenlem  6963  domtriord  7007  mapxpen  7027  mapunen  7030  ssenen  7035  nneneq  7044  onomeneq  7050  nndomo  7054  fodomfib  7136  f1opwfi  7159  elfiun  7183  suplub2  7212  ordiso2  7230  ordiso  7231  oieu  7254  brwdom2  7287  brwdom3  7296  cantnfreslem  7377  cantnflem1  7391  cardidm  7592  carddom2  7610  pm54.43  7633  pr2ne  7635  acnen  7680  acnen2  7682  alephord  7702  alephinit  7722  dfac5  7755  infdif2  7836  fictb  7871  coflim  7887  fincssdom  7949  fin23lem25  7950  isf32lem9  7987  isf34lem4  8003  fin1a2lem11  8036  axdc3lem2  8077  ficard  8187  fpwwe2lem12  8263  fpwwe2  8265  indpi  8531  nqereq  8559  1idpr  8653  ltapr  8669  leltne  8911  ltlen  8922  ltadd2  8924  ltord1  9299  mul0or  9408  ltmul1  9606  lt2msq  9640  nnsub  9784  nn0sub  10014  zrevaddcl  10063  zltp1le  10067  zdiv  10082  nneo  10095  zeo2  10098  zmax  10313  zbtwnre  10314  qrevaddcl  10338  xrlttri  10473  xrleltne  10479  xralrple  10532  xltneg  10544  xleadd1  10575  xlemul1  10610  supxrunb1  10638  supxrunb2  10639  ioo0  10681  iccid  10701  ico0  10702  ioc0  10703  icc0  10704  difreicc  10767  iccsplit  10768  0fz1  10813  uzsplit  10855  fzm1  10862  fzrevral  10866  flge  10937  modid2  10994  seqf1olem1  11085  hashen  11346  hashdom  11361  shftlem  11563  shftuz  11564  abslt  11798  absle  11799  rexico  11837  cau3lem  11838  rlim2lt  11971  rlim3  11972  o1lo1  12011  rlimdm  12025  climshft  12050  o1dif  12103  isercolllem2  12139  isercoll  12141  zsum  12191  fsum  12193  fsum00  12256  incexclem  12295  dvdsval2  12534  moddvds  12538  negdvdsb  12545  dvdsnegb  12546  dvdscmulr  12557  dvdsmulcr  12558  dvdssub2  12566  fzo0dvdseq  12581  bitsf1ocnv  12635  sadcaddlem  12648  bitsuz  12665  dvdsgcdb  12723  gcdeq  12731  dvdssqlem  12738  isprm2lem  12765  dvdsprime  12771  dvdsprm  12778  coprm  12779  euclemma  12787  rpexp  12799  prmdiveq  12854  odzdvds  12860  pythagtrip  12887  pc2dvds  12931  pcprmpw2  12934  pcprmpw  12935  vdwapun  13021  ramtcl2  13058  firest  13337  mrieqv2d  13541  isacs2  13555  isssc  13697  setciso  13923  posasymb  14086  pleval2  14099  pltval3  14101  lubid  14116  joinle  14127  meetle  14134  lubun  14227  clatleglb  14230  latdisd  14293  letsr  14349  gsumval2a  14459  frmdss2  14485  isgrpid2  14518  isgrpinv  14532  oddvdsnn0  14859  oddvds  14862  odeq  14865  odeq1  14873  gexdvds  14895  pgpfi  14916  pgpssslw  14925  fislw  14936  sylow3lem2  14939  lsmelvalm  14962  lsmlub  14974  lsmss1b  14976  lsmss2b  14978  efgs1b  15045  cyggenod  15171  cyggexb  15185  dprdfeq0  15257  unitmulclb  15447  dvreq1  15475  drngmul0or  15533  isabvd  15585  issrngd  15626  lssats2  15757  lspsneq0  15769  lsmelval2  15838  lvecvs0or  15861  lspsneq  15875  lspsneu  15876  lidl1el  15970  lidldvgen  16007  isnzr2  16015  rrgeq0  16031  domneq0  16038  znunit  16517  ipeq0  16542  ocvsscon  16575  pjdm2  16611  obselocv  16628  unitg  16705  tgss3  16724  clsval2  16787  isopn3  16803  elcls3  16820  opncldf1  16821  neiint  16841  neips  16850  opnneissb  16851  opnssneib  16852  opnnei  16857  tpnei  16858  opnneiid  16863  restcld  16903  restopnb  16906  tgcn  16982  tgcnp  16983  subbascn  16984  cnpnei  16993  cncls2  17002  cncls  17003  cnntr  17004  lmss  17026  hausnei2  17081  lpcls  17092  ordtt1  17107  cmpsub  17127  tgcmp  17128  1stcelcls  17187  kgencn2  17252  ptpjpre1  17266  upxp  17317  txcn  17320  txlm  17342  tgqtop  17403  kqfvima  17421  isr0  17428  regr1lem2  17431  hmeoopn  17457  hmeocld  17458  ptuncnv  17498  fbunfip  17564  fgss2  17569  ufilb  17601  ufprim  17604  trufil  17605  cfinufil  17623  ufildr  17626  elfm2  17643  elfm3  17645  rnelfm  17648  fmfnfmlem4  17652  fmco  17656  flimtopon  17665  flimopn  17670  fbflim2  17672  flimrest  17678  flffbas  17690  cnpflf  17696  fclstopon  17707  fclsnei  17714  fclsbas  17716  fclsfnflim  17722  fclscmp  17725  ufilcmp  17727  isfcf  17729  fcfnei  17730  cnpfcf  17736  alexsubb  17740  alexsubALT  17745  cldsubg  17793  tgphaus  17799  tgpt0  17801  tsmsgsum  17821  tsmsres  17826  xbln0  17965  blssex  17973  isxms2  17994  prdsbl  18037  neibl  18047  metss  18054  met2ndc  18069  metrest  18070  metcnp3  18086  nmoeq0  18245  xrsxmet  18315  reconn  18333  iccpnfcnv  18442  fgcfil  18697  iscau4  18705  cfilres  18722  iunmbl2  18914  ismbf3d  19009  mbfaddlem  19015  i1faddlem  19048  i1fmullem  19049  ellimc3  19229  tdeglem4  19446  deg1nn0clb  19476  deg1lt0  19477  dvdsq1p  19546  plypf1  19594  0dgrb  19628  plymul0or  19661  ulmshft  19769  ulmcaulem  19771  ulmcau  19772  cosord  19894  eff1olem  19910  lognegb  19943  eflogeq  19955  logdivlt  19972  efopn  20005  cxpeq0  20025  cxpeq  20097  angpieqvd  20128  dcubic  20142  asinsinb  20193  acoscosb  20194  atantanb  20220  rlimcnp  20260  isppw  20352  isppw2  20353  vmappw  20354  isnsqf  20373  ppieq0  20414  fsumdvdsdiag  20424  dvdsppwf1o  20426  fsumfldivdiag  20430  chpeq0  20447  chteq0  20448  dchrptlem1  20503  lgsdir2lem4  20565  lgsne0  20572  lgsqr  20585  lgsdchrval  20586  lgsquadlem1  20593  m1lgs  20601  grpoinvf  20907  rngosn3  21093  rngosn4  21094  rngoueqz  21097  nvmul0or  21210  nvz  21235  diporthcom  21292  ubthlem3  21451  hvmul0or  21604  his6  21678  hial0  21681  hial02  21682  orthcom  21687  normgt0  21706  ocin  21875  occon3  21876  shsel3  21894  shlub  21993  chssoc  22075  h1de2bi  22133  spansncol  22147  elspansn4  22152  spansnss2  22154  sumspansn  22228  lnopcnbd  22616  lnfncnbd  22637  riesz1  22645  elpjrn  22770  cvcon3  22864  dmdmd  22880  dmdbr3  22885  dmdbr4  22886  dmdbr5  22888  mdslmd1i  22909  atcveq0  22928  chcv1  22935  atssma  22958  atcv0eq  22959  atcv1  22960  funimass4f  23042  ballotlemsf1o  23072  eliccioo  23115  bisimpd  23120  bian1d  23122  eliccelico  23270  elicoelioo  23271  unitdivcld  23285  xaddeq0  23304  xrsinvgval  23306  xrge0iifcnv  23315  disjabrex  23359  disjabrexf  23360  lmxrge0  23375  imambfm  23567  indf1ofs  23609  orvcgteel  23668  orvclteel  23673  dstfrvunirn  23675  cvmliftmolem2  23813  cvmlift2lem12  23845  eupath2lem3  23903  ghomf1olem  24001  climuzcnv  24004  relexpindlem  24036  mulge0b  24086  br8  24113  br6  24114  br4  24115  funbreq  24127  fprb  24129  axext4dist  24157  nodenselem8  24342  dfrdg4  24488  brbtwn  24527  brcgr  24528  brbtwn2  24533  axcontlem7  24598  cgrcom  24613  cgrcoml  24619  cgrdegen  24627  btwncom  24637  brsegle  24731  brsegle2  24732  colinbtwnle  24741  btwnoutside  24748  broutsideof3  24749  outsidele  24755  lineunray  24770  lineelsb2  24771  elhf2  24805  ontgval  24870  ordtop  24875  ordcmp  24886  nndivsub  24896  wl-bibi1  24913  copsexgb  24966  boxbid  25011  nxtbid  25012  diabid  25013  untbi12d  25022  domrngref  25060  domintreflemb  25062  f1ofi  25070  twsymr  25078  injrec2  25119  surjsec2  25120  repcpwti  25161  cbicp  25166  dupre1  25243  inposet  25278  dffprod  25319  grpodivfo  25374  trran2  25393  ltrran2  25403  rltrran  25414  rngoridfz  25437  svli2  25484  svs2  25487  cldifemp  25524  iscnp4  25563  limptlimpr  25576  flfnei2  25577  iint  25612  trran  25614  dmrngcmp  25751  ismonc  25814  isepic  25824  sgplpte21e  26137  xsyysx  26145  pdiveql  26168  abhp  26173  elicc3  26228  nn0prpwlem  26238  opnbnd  26243  cldbnd  26244  opnregcld  26248  cldregopn  26249  fnessref  26293  refssfne  26294  locfincmp  26304  neibastop2  26310  fnemeet2  26316  fnejoin2  26318  fgmin  26319  brabg2  26366  istotbnd3  26495  sstotbnd2  26498  sstotbnd  26499  sstotbnd3  26500  ssbnd  26512  ismtybnd  26531  reheibor  26563  grpoeqdivid  26571  grpokerinj  26575  1idl  26651  0rngo  26652  divrngidl  26653  igenval2  26691  ispridlc  26695  isdmn3  26699  prtlem10  26733  prter2  26749  ralxpmap  26761  elrfi  26769  diophrw  26838  eldioph2b  26842  diophin  26852  rexrabdioph  26875  rmxycomplete  27002  coprmdvdsb  27074  jm2.19  27086  jm2.26  27095  jm2.27  27101  limsuc2  27137  islinds4  27305  dgraa0p  27354  rngunsnply  27378  fiuneneq  27513  hashgcdlem  27516  dvconstbi  27551  expgrowth  27552  ax10ext  27606  pm14.24  27632  sbiota1  27634  sigarcol  27854  rexsb  27946  2reu2  27965  ralbinrald  27977  nbusgra  28143  nbcusgra  28159  uvtxnbgra  28165  frgra3vlem2  28179  sbcim2g  28302  bnj145  28755  ax9lem2  29141  lubunNEW  29163  lshpinN  29179  lsatcveq0  29222  lsatcv0eq  29237  lsatcv1  29238  islshpcv  29243  lkr0f  29284  lkrshp4  29298  lshpkrlem1  29300  lshpset2N  29309  lfl1dim  29311  lfl1dim2N  29312  lub0N  29379  glb0N  29383  oplecon3b  29390  cmtcomN  29439  cmtbr3N  29444  cmtbr4N  29445  cvrnbtwn2  29465  cvrnbtwn3  29466  cvrcon3b  29467  cvrnbtwn4  29469  cvrcmp  29473  atcvreq0  29504  atnle  29507  atlatle  29510  cvlexchb1  29520  cvlcvr1  29529  hlrelat2  29592  exatleN  29593  cvrval3  29602  cvrval4N  29603  cvrexch  29609  atcvr0eq  29615  lnnat  29616  atcvrj0  29617  atcvrj2b  29621  atltcvr  29624  atbtwn  29635  ps-1  29666  3at  29679  islln2a  29706  llncmp  29711  islpln2a  29737  lplncmp  29751  islvol2aN  29781  4at  29802  lvolcmp  29806  pmaple  29950  lncmp  29972  paddss  30034  llnexchb2lem  30057  2polcon4bN  30107  ispsubcl2N  30136  lhpat3  30235  lautcvr  30281  ltrnid  30324  trlval2  30352  trlatn0  30361  ltrnideq  30364  trlnidatb  30366  cdlemeg49lebilem  30728  trlord  30758  cdlemg1a  30759  cdlemg1cex  30777  tendoid0  31014  dva1dim  31174  cdlemm10N  31308  diarnN  31319  cdlemn  31402  dihlspsnssN  31522  dihatexv  31528  dochkrshp  31576  dochkrshp4  31579  djhlsmcl  31604  lcfl6  31690  lcfl8  31692  lcfrvalsnN  31731  lcfrlem9  31740  mapdval2N  31820  mapdordlem2  31827  mapd1o  31838  mapd0  31855  mapdheq2biN  31920
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