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

Theorem impbida 832
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 434 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 impbida.2 . . 3  |-  ( (
ph  /\  ch )  ->  ps )
43ex 434 . 2  |-  ( ph  ->  ( ch  ->  ps ) )
52, 4impbid 191 1  |-  ( ph  ->  ( ps  <->  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369
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  df-an 371
This theorem is referenced by:  eqrdav  2441  eqrdavOLD  2442  frsn  5060  funfvbrb  5985  iinpreima  6002  fnprb  6114  fnprOLD  6115  nvocnv  6172  f1ocnv2d  6511  el2xptp0  6829  1stconst  6873  2ndconst  6874  cnvf1o  6884  tfrlem15  7063  oeeui  7253  ersymb  7327  swoer  7341  erth  7358  boxriin  7513  boxcutc  7514  domunsncan  7619  pw2f1olem  7623  enen1  7659  enen2  7660  domen1  7661  domen2  7662  sdomen1  7663  sdomen2  7664  xpmapenlem  7686  ordiso2  7943  wdomen1  8005  wdomen2  8006  fin23lem26  8708  fpwwe2lem8  9018  r1wunlim  9118  ixxun  11554  xov1plusxeqvd  11675  fzsplit2  11719  fseq1p1m1  11761  elfz2nn0  11777  flflp1  11923  modsubdir  12034  zesq  12268  hashprg  12439  hashgt0elexb  12446  hashbclem  12480  rereb  12932  rlimclim  13348  iserex  13458  caucvgb  13481  mptfzshft  13572  fsumrev  13573  climcnds  13642  dvdsadd2b  13905  bitsfzo  13962  dvdsmulgcd  14069  qden1elz  14167  mrcidb  14889  mrieqvlemd  14903  isacs2  14927  ssclem  15065  issubc3  15092  ffthiso  15172  fuciso  15218  setcmon  15288  setcepi  15289  setcinv  15291  catciso  15308  acsfiindd  15681  issubmnd  15822  mhmf1o  15850  subsubm  15862  resmhm2b  15866  grpinvid1  15972  grpinvid2  15973  subsubg  16098  ssnmz  16117  ghmf1  16169  ghmf1o  16170  conjnmzb  16175  subggim  16188  gicsubgen  16200  gass  16213  odf1  16458  gex1  16485  fislw  16519  sylow3lem2  16522  sylow3lem6  16526  lsmdisj2a  16579  lsmdisj2b  16580  efgred2  16645  dmdprdsplit  16970  0unit  17203  irrednegb  17234  rhmf1o  17255  kerf1hrm  17266  isdrng2  17280  subrgunit  17321  issubdrg  17328  subsubrg  17329  islss3  17479  islss4  17482  lspsnel6  17514  lspsneq0b  17533  islmhm2  17558  lmhmf1o  17566  reslmhm2b  17574  lssvs0or  17630  lvecinv  17633  lspsnel4  17644  lspdisjb  17646  islbs2  17674  islbs3  17675  issubassa  17847  issubassa2  17868  gsumbagdiag  17902  subrgasclcl  18038  prmirredlem  18396  prmirredlemOLD  18399  islindf3  18734  lindsmm  18736  lsslindf  18738  lsslinds  18739  matunit  19053  slesolinvbi  19056  en2top  19360  elcls  19447  neindisj2  19497  neiptopnei  19506  neiptopreu  19507  maxlp  19521  neitr  19554  iscncl  19643  cncnp  19654  isreg2  19751  dis2ndc  19834  1stccnp  19836  islly2  19858  dislly  19871  dissnlocfin  19903  kgencmp2  19920  pt1hmeo  20180  xkocnv  20188  t0kq  20192  uffixfr  20297  flimcf  20356  cnpflf2  20374  fclscf  20399  cnextf  20439  utopsnneiplem  20623  isucn2  20655  cfilucfilOLD  20945  cfilucfil  20946  metutopOLD  20958  psmetutop  20959  restmetu  20963  tngngp2  21039  tngngp  21041  nmoleub  21111  metdseq0  21231  cnheibor  21328  pcophtb  21402  nmoleub2lem  21470  lmmbr  21570  iscfil3  21585  cmetss  21626  cldcss  21729  mbfeqalem  21922  mbfposb  21933  itg2const2  22021  itgss3  22094  plyco0  22462  dgrlt  22535  ulm2  22652  coseq00topi  22767  coseq0negpitopi  22768  sineq0  22786  atans2  23134  xrlimcnp  23170  dchrelbas2  23384  dchrn0  23397  2sqb  23525  istrkg2ld  23730  tgcgreqb  23744  tgbtwncomb  23752  trgcgrg  23778  legov  23844  legov2  23845  legov3  23856  hlbtwn  23867  tglineelsb2  23884  tglinecom  23887  colline  23902  mirinv  23919  mirbtwnb  23924  mirbtwnhl  23932  perpcom  23962  isperp2  23964  oppcom  23988  opphllem3  23993  lnopp2hpgb  24004  lmieu  24022  nb3graprlem1  24323  eleclclwwlknlem2  24690  clwwlknscsh  24691  el2spthonot0  24743  numclwwlk2lem1  24974  grpoinvid1  25104  grpoinvid2  25105  ismndo1  25218  leopmul  26925  hst1h  27018  disjabrex  27315  disjabrexf  27316  erbr3b  27340  f1o3d  27343  funimass4f  27346  fgreu  27385  fcnvgreu  27386  fcobij  27420  resf1o  27425  mul2lt0bi  27441  fzsplit3  27471  eliccioo  27500  ogrpinv0le  27579  ogrpaddltbi  27582  ogrpaddltrbid  27584  ogrpinv0lt  27586  isarchi3  27604  fimaproj  27709  qtophaus  27712  reff  27715  locfinreflem  27716  cmpcref  27726  metider  27746  pstmfval  27748  qqhval2  27836  aean  28089  imambfm  28106  eulerpartlemgvv  28188  orvcgteel  28279  orvclteel  28284  ballotlemsf1o  28325  sgn3da  28353  sgnnbi  28357  sgnpbi  28358  sgnmulsgn  28361  sgnmulsgp  28362  sconpi1  28557  fprodrev  29082  brofs2  29702  brifs2  29703  broutsideof2  29747  ltflcei  30018  ismblfin  30030  cnambfre  30038  ftc1anclem6  30070  isdrngo2  30336  mrefg2  30614  mzpmfp  30654  mzpmfpOLD  30655  lzenom  30678  elpell14qr2  30773  elpell1qr2  30783  pellfund14b  30810  congabseq  30887  acongeq  30896  jm2.23  30913  jm2.20nn  30914  jm2.25lem1  30915  wepwsolem  30962  islssfg2  30992  lnmlmic  31009  dfacbasgrp  31032  lcmgcdeq  31192  rfcnpre3  31362  rfcnpre4  31363  ioossioobi  31493  iccshift  31494  iocopn  31496  eliccelioc  31497  iooshift  31498  icoopn  31501  limcdm0  31532  islptre  31533  islpcn  31553  limcresioolb  31557  fperdvper  31619  itgperiod  31670  fourierdlem32  31810  fourierdlem33  31811  fourierdlem48  31826  fourierdlem49  31827  fourierdlem71  31849  fourierdlem81  31859  mgmhmf1o  32313  issubmgm2  32316  subsubmgm  32323  resmgmhm2b  32326  rnghmf1o  32424  rngcinv  32526  rngcinvOLD  32538  ringcinv  32572  ringcinvOLD  32596  lshpnelb  34443  lshpnel2N  34444  lsatspn0  34459  lsatelbN  34465  lsat0cv  34492  lcvexch  34498  lcv1  34500  lkrshp3  34565  lkrpssN  34622  lkrss2N  34628  cvlsupr2  34802  atcvrlln  34978  llncvrlpln  35016  2llnmj  35018  lplncvrlvol  35074  2lplnmj  35080  polcon2bN  35378  pcl0bN  35381  lhpmcvr3  35483  lhpmatb  35489  ltrncoidN  35586  ltrneq3  35667  ltrniotavalbN  36044  cdlemg1cN  36047  diclspsn  36655  dihopelvalcpre  36709  dihord4  36719  dihord  36725  dihmeetlem4preN  36767  dih1dimatlem0  36789  dochsscl  36829  dochoccl  36830  dochord  36831  dochsat  36844  dochshpncl  36845  dochsatshpb  36913  dochshpsat  36915  mapdval4N  37093  mapdsn  37102  hdmap14lem12  37343  hdmapip0  37379  hlhillcs  37422
  Copyright terms: Public domain W3C validator