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

Theorem impbid 184
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 183 . 2  |-  ( ph  ->  ( ph  ->  ( ps 
<->  ch ) ) )
43pm2.43i 45 1  |-  ( ph  ->  ( ps  <->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  bicom1  191  impbid1  195  impcon4bid  197  pm5.74  236  imbi1d  309  pm5.501  331  2falsed  341  impbida  806  dedlem0b  920  dedlema  921  dedlemb  922  albi  1570  exbi  1588  equequ1  1691  equequ1OLD  1692  elequ1  1720  elequ2  1722  19.21t  1803  19.23t  1808  19.23tOLD  1828  19.21tOLD  1875  sbequ12  1933  dral1  1991  cbv2h  2006  ax11b  2021  sbft  2051  sbied  2062  sbequ  2086  sb56  2124  sbal1  2153  exsb  2157  dral1-o  2181  eupickb  2296  eupickbi  2297  2eu2  2312  ceqsalt  2914  ceqex  3002  mob2  3050  reu6  3059  sbciegft  3127  eqsbc3r  3154  csbiebt  3223  sseq1  3305  reupick  3561  reupick2  3563  uneqdifeq  3652  prnebg  3914  disjeq2  4120  disjeq1  4123  disjxiun  4143  disjss3  4145  copsexg  4376  euotd  4391  poeq2  4441  sotric  4463  sotrieq  4464  freq2  4487  seeq1  4488  seeq2  4489  tz7.7  4541  ordtri1  4548  ordtri3  4551  ordelinel  4613  reusv2lem2  4658  reusv2lem3  4659  alxfr  4669  ralxfrd  4670  oneqmin  4718  ordsuc  4727  ordelsuc  4733  ordsucelsuc  4735  ordunisuc2  4757  limsuc  4762  iss  5122  iotaval  5362  funeq  5406  funssres  5426  tz6.12c  5683  fnbrfvb  5699  ssimaex  5720  fvimacnv  5777  elpreima  5782  eldmrexrnb  5809  fsn  5838  fconst2g  5878  fconst5  5881  elunirnALT  5932  f1ocnvfvb  5949  foeqcnvco  5959  f1eqcocnv  5960  fliftfun  5966  soisores  5979  isofr  5994  isose  5995  isopo  5998  isoso  6000  f1oiso2  6004  oprabid  6037  f1opw2  6230  op1steq  6323  rntpos  6421  eusvobj2  6511  smoiso2  6560  seqomlem2  6637  oaord  6719  oawordex  6729  oaordex  6730  omord2  6739  om00  6747  oeord  6760  nnaord  6791  nnmord  6804  nnawordex  6809  nnaordex  6810  erexb  6859  swoord1  6863  swoord2  6864  iiner  6905  eceqoveq  6938  omxpenlem  7138  domtriord  7182  mapxpen  7202  mapunen  7205  ssenen  7210  nneneq  7219  onomeneq  7225  nndomo  7229  fodomfib  7315  f1opwfi  7338  elfiun  7363  suplub2  7392  ordiso2  7410  ordiso  7411  oieu  7434  brwdom2  7467  brwdom3  7476  cantnfreslem  7557  cantnflem1  7571  cardidm  7772  carddom2  7790  pm54.43  7813  pr2ne  7815  acnen  7860  acnen2  7862  alephord  7882  alephinit  7902  dfac5  7935  infdif2  8016  fictb  8051  coflim  8067  fincssdom  8129  fin23lem25  8130  isf32lem9  8167  isf34lem4  8183  fin1a2lem11  8216  axdc3lem2  8257  ficard  8366  fpwwe2lem12  8442  fpwwe2  8444  indpi  8710  nqereq  8738  1idpr  8832  ltapr  8848  leltne  9090  ltlen  9101  ltadd2  9103  ltord1  9478  mul0or  9587  ltmul1  9785  lt2msq  9819  nnsub  9963  nn0sub  10195  zrevaddcl  10246  zltp1le  10250  zdiv  10265  nneo  10278  zeo2  10281  zmax  10496  zbtwnre  10497  qrevaddcl  10521  xrlttri  10657  xrleltne  10663  xralrple  10716  xltneg  10728  xleadd1  10759  xlemul1  10794  supxrunb1  10823  supxrunb2  10824  ioo0  10866  iccid  10886  ico0  10887  ioc0  10888  icc0  10889  difreicc  10953  iccsplit  10954  0fz1  10999  uzsplit  11041  fzm1  11050  fzrevral  11054  elfznelfzob  11113  flge  11134  modid2  11191  seqf1olem1  11282  hashen  11551  hashdom  11573  hashle00  11589  hash2prb  11609  hashtpg  11611  shftlem  11803  shftuz  11804  abslt  12038  absle  12039  rexico  12077  cau3lem  12078  rlim2lt  12211  rlim3  12212  o1lo1  12251  rlimdm  12265  climshft  12290  o1dif  12343  isercolllem2  12379  isercoll  12381  zsum  12432  fsum  12434  fsum00  12497  incexclem  12536  dvdsval2  12775  moddvds  12779  negdvdsb  12786  dvdsnegb  12787  dvdscmulr  12798  dvdsmulcr  12799  dvdssub2  12807  fzo0dvdseq  12822  bitsf1ocnv  12876  sadcaddlem  12889  bitsuz  12906  dvdsgcdb  12964  gcdeq  12972  dvdssqlem  12979  isprm2lem  13006  dvdsprime  13012  dvdsprm  13019  coprm  13020  euclemma  13028  rpexp  13040  prmdiveq  13095  odzdvds  13101  pythagtrip  13128  pc2dvds  13172  pcprmpw2  13175  pcprmpw  13176  vdwapun  13262  ramtcl2  13299  firest  13580  mrieqv2d  13784  isacs2  13798  isssc  13940  setciso  14166  posasymb  14329  pleval2  14342  pltval3  14344  lubid  14359  joinle  14370  meetle  14377  lubun  14470  clatleglb  14473  latdisd  14536  letsr  14592  gsumval2a  14702  frmdss2  14728  isgrpid2  14761  isgrpinv  14775  oddvdsnn0  15102  oddvds  15105  odeq  15108  odeq1  15116  gexdvds  15138  pgpfi  15159  pgpssslw  15168  fislw  15179  sylow3lem2  15182  lsmelvalm  15205  lsmlub  15217  lsmss1b  15219  lsmss2b  15221  efgs1b  15288  cyggenod  15414  cyggexb  15428  dprdfeq0  15500  unitmulclb  15690  dvreq1  15718  drngmul0or  15776  isabvd  15828  issrngd  15869  lssats2  15996  lspsneq0  16008  lsmelval2  16077  lvecvs0or  16100  lspsneq  16114  lspsneu  16115  lidl1el  16209  lidldvgen  16246  isnzr2  16254  rrgeq0  16270  domneq0  16277  znunit  16760  ipeq0  16785  ocvsscon  16818  pjdm2  16854  obselocv  16871  unitg  16948  tgss3  16967  clsval2  17030  isopn3  17046  elcls3  17063  opncldf1  17064  neiint  17084  neips  17093  opnneissb  17094  opnssneib  17095  opnnei  17100  tpnei  17101  opnneiid  17106  restcld  17151  restopnb  17154  tgcn  17231  tgcnp  17232  subbascn  17233  iscnp4  17242  cnpnei  17243  cncls2  17252  cncls  17253  cnntr  17254  lmss  17277  hausnei2  17332  lpcls  17343  ordtt1  17358  cmpsub  17378  tgcmp  17379  1stcelcls  17438  kgencn2  17503  ptpjpre1  17517  upxp  17569  txcn  17572  txlm  17594  tgqtop  17658  kqfvima  17676  isr0  17683  regr1lem2  17686  hmeoopn  17712  hmeocld  17713  ptuncnv  17753  fbunfip  17815  fgss2  17820  ufilb  17852  ufprim  17855  trufil  17856  cfinufil  17874  ufildr  17877  elfm2  17894  elfm3  17896  rnelfm  17899  fmfnfmlem4  17903  fmco  17907  flimtopon  17916  flimopn  17921  fbflim2  17923  flimrest  17929  flffbas  17941  cnpflf  17947  fclstopon  17958  fclsnei  17965  fclsbas  17967  fclsfnflim  17973  fclscmp  17976  ufilcmp  17978  isfcf  17980  fcfnei  17981  cnpfcf  17987  alexsubb  17991  alexsubALT  17996  cldsubg  18054  tgphaus  18060  tgpt0  18062  tsmsgsum  18082  tsmsres  18087  xbln0  18332  blssex  18340  isxms2  18361  prdsbl  18404  neibl  18414  metss  18421  met2ndc  18436  metrest  18437  metcnp3  18453  nmoeq0  18634  xrsxmet  18704  reconn  18723  iccpnfcnv  18833  fgcfil  19088  iscau4  19096  cfilres  19113  iunmbl2  19311  ismbf3d  19406  mbfaddlem  19412  i1faddlem  19445  i1fmullem  19446  ellimc3  19626  tdeglem4  19843  deg1nn0clb  19873  deg1lt0  19874  dvdsq1p  19943  plypf1  19991  0dgrb  20025  plymul0or  20058  ulmshft  20166  ulmcaulem  20170  ulmcau  20171  cosord  20294  eff1olem  20310  lognegb  20344  eflogeq  20356  logdivlt  20376  efopn  20409  cxpeq0  20429  cxpeq  20501  angpieqvd  20532  dcubic  20546  asinsinb  20597  acoscosb  20598  atantanb  20624  rlimcnp  20664  isppw  20757  isppw2  20758  vmappw  20759  isnsqf  20778  ppieq0  20819  fsumdvdsdiag  20829  dvdsppwf1o  20831  fsumfldivdiag  20835  chpeq0  20852  chteq0  20853  dchrptlem1  20908  lgsdir2lem4  20970  lgsne0  20977  lgsqr  20990  lgsdchrval  20991  lgsquadlem1  20998  m1lgs  21006  ausisusgra  21240  nbusgra  21299  nbgraf1olem5  21314  edgusgranbfin  21318  nb3graprlem1  21319  cusgrarn  21327  nbcusgra  21331  cusgrafilem2  21348  uvtxnbgra  21361  3v3e3cycl  21493  eupath2lem3  21542  grpoinvf  21669  rngosn3  21855  rngosn4  21856  rngoueqz  21859  rngoridfz  21864  nvmul0or  21974  nvz  21999  diporthcom  22056  ubthlem3  22215  hvmul0or  22368  his6  22442  hial0  22445  hial02  22446  orthcom  22451  normgt0  22470  ocin  22639  occon3  22640  shsel3  22658  shlub  22757  chssoc  22839  h1de2bi  22897  spansncol  22911  elspansn4  22916  spansnss2  22918  sumspansn  22992  lnopcnbd  23380  lnfncnbd  23401  riesz1  23409  elpjrn  23534  cvcon3  23628  dmdmd  23644  dmdbr3  23649  dmdbr4  23650  dmdbr5  23652  mdslmd1i  23673  atcveq0  23692  chcv1  23699  atssma  23722  atcv0eq  23723  atcv1  23724  bian1d  23791  eliccelico  23969  elicoelioo  23970  xaddeq0  24023  unitdivcld  24096  xrge0iifcnv  24116  lmxrge0  24134  indf1ofs  24212  dstfrvunirn  24504  cvmliftmolem2  24741  cvmlift2lem12  24773  ghomf1olem  24877  climuzcnv  24880  relexpindlem  24911  mulge0b  24963  zprod  25035  fprod  25039  br8  25130  br6  25131  br4  25132  funbreq  25144  fprb  25146  axext4dist  25174  nodenselem8  25359  dfrdg4  25506  brbtwn  25545  brcgr  25546  brbtwn2  25551  axcontlem7  25616  cgrcom  25631  cgrcoml  25637  cgrdegen  25645  btwncom  25655  brsegle  25749  brsegle2  25750  colinbtwnle  25759  btwnoutside  25766  broutsideof3  25767  outsidele  25773  lineunray  25788  lineelsb2  25789  elhf2  25823  ontgval  25888  ordtop  25893  ordcmp  25904  nndivsub  25914  wl-bibi1  25930  itg2addnc  25952  elicc3  26004  nn0prpwlem  26009  opnbnd  26012  cldbnd  26013  opnregcld  26017  cldregopn  26018  fnessref  26057  refssfne  26058  locfincmp  26068  neibastop2  26074  fnemeet2  26080  fnejoin2  26082  fgmin  26083  brabg2  26101  istotbnd3  26164  sstotbnd2  26167  sstotbnd  26168  sstotbnd3  26169  ssbnd  26181  ismtybnd  26200  reheibor  26232  grpoeqdivid  26240  grpokerinj  26244  1idl  26320  0rngo  26321  divrngidl  26322  igenval2  26360  ispridlc  26364  isdmn3  26368  prtlem10  26398  prter2  26414  ralxpmap  26426  elrfi  26432  diophrw  26501  eldioph2b  26505  diophin  26515  rexrabdioph  26538  rmxycomplete  26664  coprmdvdsb  26736  jm2.19  26748  jm2.26  26757  jm2.27  26763  limsuc2  26799  islinds4  26967  dgraa0p  27016  rngunsnply  27040  fiuneneq  27175  hashgcdlem  27178  dvconstbi  27213  expgrowth  27214  ax10ext  27268  pm14.24  27294  sbiota1  27296  sigarcol  27515  rexsb  27607  2reu2  27626  ralbinrald  27638  rlimdmafv  27703  frgra3vlem2  27747  frgrancvvdeqlem3  27777  sbcim2g  27959  bnj145  28425  dral1NEW7  28824  cbv2hwAUX7  28844  sbiedNEW7  28869  sbftNEW7  28885  sbequNEW7  28908  sb56NEW7  28922  exsbNEW7  28925  sbal1NEW7  28941  ax11bNEW7  28948  cbv2hOLD7  29030  ax9lem2  29117  lubunNEW  29139  lshpinN  29155  lsatcveq0  29198  lsatcv0eq  29213  lsatcv1  29214  islshpcv  29219  lkr0f  29260  lkrshp4  29274  lshpkrlem1  29276  lshpset2N  29285  lfl1dim  29287  lfl1dim2N  29288  lub0N  29355  glb0N  29359  oplecon3b  29366  cmtcomN  29415  cmtbr3N  29420  cmtbr4N  29421  cvrnbtwn2  29441  cvrnbtwn3  29442  cvrcon3b  29443  cvrnbtwn4  29445  cvrcmp  29449  atcvreq0  29480  atnle  29483  atlatle  29486  cvlexchb1  29496  cvlcvr1  29505  hlrelat2  29568  exatleN  29569  cvrval3  29578  cvrval4N  29579  cvrexch  29585  atcvr0eq  29591  lnnat  29592  atcvrj0  29593  atcvrj2b  29597  atltcvr  29600  atbtwn  29611  ps-1  29642  3at  29655  islln2a  29682  llncmp  29687  islpln2a  29713  lplncmp  29727  islvol2aN  29757  4at  29778  lvolcmp  29782  pmaple  29926  lncmp  29948  paddss  30010  llnexchb2lem  30033  2polcon4bN  30083  ispsubcl2N  30112  lhpat3  30211  lautcvr  30257  ltrnid  30300  trlval2  30328  trlatn0  30337  ltrnideq  30340  trlnidatb  30342  cdlemeg49lebilem  30704  trlord  30734  cdlemg1a  30735  cdlemg1cex  30753  tendoid0  30990  dva1dim  31150  cdlemm10N  31284  diarnN  31295  cdlemn  31378  dihlspsnssN  31498  dihatexv  31504  dochkrshp  31552  dochkrshp4  31555  djhlsmcl  31580  lcfl6  31666  lcfl8  31668  lcfrvalsnN  31707  lcfrlem9  31716  mapdval2N  31796  mapdordlem2  31803  mapd1o  31814  mapd0  31831  mapdheq2biN  31896
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 178
  Copyright terms: Public domain W3C validator