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

Theorem impbida 842
Description: Deduce an equivalence from two implications. (Contributed by NM, 17-Feb-2007.)
Hypotheses
Ref Expression
impbida.1  |-  ( (
ph  /\  ps )  ->  ch )
impbida.2  |-  ( (
ph  /\  ch )  ->  ps )
Assertion
Ref Expression
impbida  |-  ( ph  ->  ( ps  <->  ch )
)

Proof of Theorem impbida
StepHypRef Expression
1 impbida.1 . . 3  |-  ( (
ph  /\  ps )  ->  ch )
21ex 436 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 impbida.2 . . 3  |-  ( (
ph  /\  ch )  ->  ps )
43ex 436 . 2  |-  ( ph  ->  ( ch  ->  ps ) )
52, 4impbid 194 1  |-  ( ph  ->  ( ps  <->  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    /\ wa 371
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 189  df-an 373
This theorem is referenced by:  eqrdav  2449  frsn  4904  elsnxp  5377  funfvbrb  5993  iinpreima  6008  fnprb  6121  fpr2g  6123  nvocnv  6178  fsnex  6179  f1prex  6180  f1ocnv2d  6517  el2xptp0  6834  1stconst  6881  2ndconst  6882  cnvf1o  6892  tfrlem15  7107  oeeui  7300  ersymb  7374  swoer  7388  erth  7405  boxriin  7561  boxcutc  7562  domunsncan  7669  pw2f1olem  7673  enen1  7709  enen2  7710  domen1  7711  domen2  7712  sdomen1  7713  sdomen2  7714  xpmapenlem  7736  ordiso2  8027  wdomen1  8088  wdomen2  8089  fin23lem26  8752  fpwwe2lem8  9059  r1wunlim  9159  mul2lt0bi  11399  ixxun  11648  xov1plusxeqvd  11775  fzsplit2  11821  fseq1p1m1  11865  elfz2nn0  11882  flflp1  12040  modsubdir  12155  zesq  12392  hashprg  12569  hashgt0elexb  12576  hashbclem  12612  hashge2el2difb  12636  rereb  13176  rlimclim  13603  iserex  13713  caucvgb  13739  mptfzshft  13832  fsumrev  13833  climcnds  13902  fprodrev  14024  dvdsadd2b  14340  bitsfzo  14402  dvdsmulgcd  14515  lcmgcdeq  14570  qden1elz  14699  mrcidb  15514  mrieqvlemd  15528  isacs2  15552  cicer  15704  ssclem  15717  issubc3  15747  ffthiso  15827  fuciso  15873  setcmon  15975  setcepi  15976  setcinv  15978  catciso  15995  acsfiindd  16416  issubmnd  16557  mhmf1o  16585  subsubm  16597  resmhm2b  16601  grpinvid1  16707  grpinvid2  16708  subsubg  16833  ssnmz  16852  ghmf1  16904  ghmf1o  16905  conjnmzb  16910  subggim  16923  gicsubgen  16935  gass  16948  odf1  17206  gex1  17236  fislw  17270  sylow3lem2  17273  sylow3lem6  17277  lsmdisj2a  17330  lsmdisj2b  17331  efgred2  17396  dmdprdsplit  17673  0unit  17901  irrednegb  17932  rhmf1o  17953  kerf1hrm  17964  isdrng2  17978  subrgunit  18019  issubdrg  18026  subsubrg  18027  islss3  18175  islss4  18178  lspsnel6  18210  lspsneq0b  18229  islmhm2  18254  lmhmf1o  18262  reslmhm2b  18270  lssvs0or  18326  lvecinv  18329  lspsnel4  18340  lspdisjb  18342  islbs2  18370  islbs3  18371  issubassa  18541  issubassa2  18562  gsumbagdiag  18593  subrgasclcl  18715  prmirredlem  19057  islindf3  19377  lindsmm  19379  lsslindf  19381  lsslinds  19382  matunit  19696  slesolinvbi  19699  en2top  19994  elcls  20082  neindisj2  20132  neiptopnei  20141  neiptopreu  20142  maxlp  20156  neitr  20189  iscncl  20278  cncnp  20289  isreg2  20386  dis2ndc  20468  1stccnp  20470  islly2  20492  dislly  20505  dissnlocfin  20537  kgencmp2  20554  pt1hmeo  20814  xkocnv  20822  t0kq  20826  uffixfr  20931  flimcf  20990  cnpflf2  21008  fclscf  21033  cnextf  21074  utopsnneiplem  21255  isucn2  21287  cfilucfil  21567  psmetutop  21575  restmetu  21578  tngngp2  21653  tngngp  21655  nmoleub  21729  nmoleubOLD  21745  metdseq0  21864  metdseq0OLD  21879  cnheibor  21976  pcophtb  22053  nmoleub2lem  22121  lmmbr  22221  iscfil3  22236  cmetss  22277  cldcss  22388  mbfeqalem  22591  mbfposb  22602  itg2const2  22692  itgss3  22765  plyco0  23139  dgrlt  23213  ulm2  23333  coseq00topi  23450  coseq0negpitopi  23451  sineq0  23469  relogbcxpb  23717  atans2  23850  xrlimcnp  23887  dchrelbas2  24158  dchrn0  24171  2sqb  24299  istrkg2ld  24501  tgcgreqb  24518  tgbtwncomb  24526  trgcgrg  24553  legov  24623  legov2  24624  legov3  24636  hlbtwn  24649  tglineelsb2  24670  tglinecom  24673  colline  24687  mirinv  24704  mirbtwnb  24710  mirbtwnhl  24718  perpcom  24751  isperp2  24753  oppcom  24779  opphllem3  24784  lnopp2hpgb  24798  colopp  24804  colhp  24805  lmieu  24819  iscgra1  24845  dfcgra2  24864  nb3graprlem1  25172  eleclclwwlknlem2  25539  clwwlknscsh  25540  el2spthonot0  25592  numclwwlk2lem1  25823  grpoinvid1  25951  grpoinvid2  25952  ismndo1  26065  leopmul  27780  hst1h  27873  disjabrex  28185  disjabrexf  28186  erbr3b  28216  f1o3d  28222  funimass4f  28227  fgreu  28267  fcnvgreu  28268  1stpreimas  28279  fcobij  28303  resf1o  28308  fzsplit3  28363  eliccioo  28393  ogrpinv0le  28472  ogrpaddltbi  28475  ogrpaddltrbid  28477  ogrpinv0lt  28479  isarchi3  28497  1smat1  28623  fimaproj  28653  qtophaus  28656  reff  28659  locfinreflem  28660  cmpcref  28670  metider  28690  pstmfval  28692  qqhval2  28779  aean  29060  imambfm  29077  eulerpartlemgvv  29202  orvcgteel  29293  orvclteel  29298  ballotlemsf1o  29339  ballotlemsf1oOLD  29377  sgn3da  29405  sgnnbi  29409  sgnpbi  29410  sgnmulsgn  29413  sgnmulsgp  29414  sconpi1  29955  brofs2  30837  brifs2  30838  broutsideof2  30882  ltflcei  31926  poimirlem25  31958  ismblfin  31974  cnambfre  31982  ftc1anclem6  32015  isdrngo2  32190  lshpnelb  32544  lshpnel2N  32545  lsatspn0  32560  lsatelbN  32566  lsat0cv  32593  lcvexch  32599  lcv1  32601  lkrshp3  32666  lkrpssN  32723  lkrss2N  32729  cvlsupr2  32903  atcvrlln  33079  llncvrlpln  33117  2llnmj  33119  lplncvrlvol  33175  2lplnmj  33181  polcon2bN  33479  pcl0bN  33482  lhpmcvr3  33584  lhpmatb  33590  ltrncoidN  33687  ltrneq3  33768  ltrniotavalbN  34145  cdlemg1cN  34148  diclspsn  34756  dihopelvalcpre  34810  dihord4  34820  dihord  34826  dihmeetlem4preN  34868  dih1dimatlem0  34890  dochsscl  34930  dochoccl  34931  dochord  34932  dochsat  34945  dochshpncl  34946  dochsatshpb  35014  dochshpsat  35016  mapdval4N  35194  mapdsn  35203  hdmap14lem12  35444  hdmapip0  35480  hlhillcs  35523  mrefg2  35543  mzpmfp  35583  lzenom  35606  elpell14qr2  35702  elpell1qr2  35712  pellfund14b  35741  congabseq  35818  acongeq  35827  jm2.23  35845  jm2.20nn  35846  jm2.25lem1  35847  wepwsolem  35894  islssfg2  35923  lnmlmic  35940  dfacbasgrp  35961  rfcnpre3  37348  rfcnpre4  37349  ioossioobi  37612  iccshift  37613  iocopn  37615  eliccelioc  37616  iooshift  37617  icoopn  37620  limcdm0  37692  islptre  37693  islpcn  37713  limcresioolb  37718  fperdvper  37784  itgperiod  37852  fourierdlem32  37996  fourierdlem33  37997  fourierdlem48  38012  fourierdlem49  38013  fourierdlem71  38035  fourierdlem81  38045  m1mod0mod1  38717  edgnbusgreu  39424  nb3grprlem1  39437  mgmhmf1o  39774  issubmgm2  39777  subsubmgm  39784  resmgmhm2b  39787  rnghmf1o  39890  rngcinv  39970  rngcinvALTV  39982  ringcinv  40021  ringcinvALTV  40045  nn0ob  40317
  Copyright terms: Public domain W3C validator