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

Theorem impbida 828
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  2437  frsn  4904  funfvbrb  5811  iinpreima  5828  fnprb  5931  fnprOLD  5932  nvocnv  5983  f1ocnv2d  6306  1stconst  6656  2ndconst  6657  cnvf1o  6666  tfrlem15  6843  oeeui  7033  ersymb  7107  swoer  7121  erth  7137  boxriin  7297  boxcutc  7298  domunsncan  7403  pw2f1olem  7407  enen1  7443  enen2  7444  domen1  7445  domen2  7446  sdomen1  7447  sdomen2  7448  xpmapenlem  7470  ordiso2  7721  wdomen1  7783  wdomen2  7784  fin23lem26  8486  fpwwe2lem8  8796  r1wunlim  8896  ixxun  11308  xov1plusxeqvd  11423  fzsplit2  11466  elfz2nn0  11472  fseq1p1m1  11526  modsubdir  11759  zesq  11979  hashprg  12147  hashgt0elexb  12152  hashbclem  12197  rereb  12601  rlimclim  13016  iserex  13126  caucvgb  13149  mptfzshft  13237  fsumrev  13238  climcnds  13306  dvdsadd2b  13567  bitsfzo  13623  dvdsmulgcd  13730  qden1elz  13827  mrcidb  14545  mrieqvlemd  14559  isacs2  14583  ssclem  14724  issubc3  14751  ffthiso  14831  fuciso  14877  setcmon  14947  setcepi  14948  setcinv  14950  catciso  14967  acsfiindd  15339  issubmnd  15441  subsubm  15476  resmhm2b  15480  grpinvid1  15577  grpinvid2  15578  subsubg  15695  ssnmz  15714  ghmf1  15766  ghmf1o  15767  conjnmzb  15772  subggim  15785  gicsubgen  15797  gass  15810  odf1  16054  gex1  16081  fislw  16115  sylow3lem2  16118  sylow3lem6  16122  lsmdisj2a  16175  lsmdisj2b  16176  efgred2  16241  dmdprdsplit  16536  0unit  16762  irrednegb  16793  isdrng2  16822  subrgunit  16863  issubdrg  16870  subsubrg  16871  islss3  17020  islss4  17023  lspsnel6  17055  lspsneq0b  17074  islmhm2  17099  lmhmf1o  17107  reslmhm2b  17115  lssvs0or  17171  lvecinv  17174  lspsnel4  17185  lspdisjb  17187  islbs2  17215  islbs3  17216  issubassa  17375  issubassa2  17395  gsumbagdiag  17426  subrgasclcl  17561  prmirredlem  17897  prmirredlemOLD  17900  islindf3  18235  lindsmm  18237  lsslindf  18239  lsslinds  18240  matunit  18464  slesolinvbi  18467  en2top  18570  elcls  18657  neindisj2  18707  neiptopnei  18716  neiptopreu  18717  maxlp  18731  neitr  18764  iscncl  18853  cncnp  18864  isreg2  18961  dis2ndc  19044  1stccnp  19046  islly2  19068  dislly  19081  kgencmp2  19099  pt1hmeo  19359  xkocnv  19367  t0kq  19371  uffixfr  19476  flimcf  19535  cnpflf2  19553  fclscf  19578  cnextf  19618  utopsnneiplem  19802  isucn2  19834  cfilucfilOLD  20124  cfilucfil  20125  metutopOLD  20137  psmetutop  20138  restmetu  20142  tngngp2  20218  tngngp  20220  nmoleub  20290  metdseq0  20410  cnheibor  20507  pcophtb  20581  nmoleub2lem  20649  lmmbr  20749  iscfil3  20764  cmetss  20805  cldcss  20908  mbfeqalem  21100  mbfposb  21111  itg2const2  21199  itgss3  21272  plyco0  21640  dgrlt  21713  ulm2  21830  coseq00topi  21944  coseq0negpitopi  21945  sineq0  21963  atans2  22306  xrlimcnp  22342  dchrelbas2  22556  dchrn0  22569  2sqb  22697  tgcgreqb  22915  tgbtwncomb  22923  trgcgrg  22947  legov  22996  legov2  22997  tglineelsb2  23018  tglinecom  23021  colline  23032  mirinv  23048  mirbtwnb  23053  perpcom  23080  isperp2  23082  nb3graprlem1  23327  grpoinvid1  23685  grpoinvid2  23686  ismndo1  23799  leopmul  25506  hst1h  25599  disjabrex  25894  disjabrexf  25895  disjunsn  25904  f1o3d  25916  funimass4f  25919  fgreu  25958  fcnvgreu  25959  mul2lt0bi  26010  fzsplit3  26046  eliccioo  26074  ogrpinv0le  26147  ogrpaddltbi  26150  ogrpaddltrbid  26152  ogrpinv0lt  26154  isarchi3  26172  kerf1hrm  26260  metider  26290  qqhval2  26380  aean  26629  imambfm  26646  eulerpartlemgvv  26728  orvcgteel  26819  orvclteel  26824  ballotlemsf1o  26865  sgn3da  26893  sgnnbi  26897  sgnpbi  26898  sgnmulsgn  26901  sgnmulsgp  26902  sconpi1  27097  fprodshft  27456  fprodrev  27457  brofs2  28077  brifs2  28078  broutsideof2  28122  ltflcei  28390  lxflflp1  28392  ismblfin  28403  cnambfre  28411  ftc1anclem6  28443  isdrngo2  28735  mrefg2  29014  mzpmfp  29054  mzpmfpOLD  29055  lzenom  29079  elpell14qr2  29174  elpell1qr2  29184  pellfund14b  29211  congabseq  29288  acongeq  29297  jm2.23  29316  jm2.20nn  29317  jm2.25lem1  29318  wepwsolem  29365  islssfg2  29395  lnmlmic  29412  dfacbasgrp  29435  rfcnpre3  29726  rfcnpre4  29727  el2xptp0  30098  el2spthonot0  30361  eleclclwwlknlem2  30462  Lemma2  30464  numclwwlk2lem1  30666  lshpnelb  32522  lshpnel2N  32523  lsatspn0  32538  lsatelbN  32544  lsat0cv  32571  lcvexch  32577  lcv1  32579  lkrshp3  32644  lkrpssN  32701  lkrss2N  32707  cvlsupr2  32881  atcvrlln  33057  llncvrlpln  33095  2llnmj  33097  lplncvrlvol  33153  2lplnmj  33159  polcon2bN  33457  pcl0bN  33460  lhpmcvr3  33562  lhpmatb  33568  ltrncoidN  33665  ltrneq3  33745  ltrniotavalbN  34121  cdlemg1cN  34124  diclspsn  34732  dihopelvalcpre  34786  dihord4  34796  dihord  34802  dihmeetlem4preN  34844  dih1dimatlem0  34866  dochsscl  34906  dochoccl  34907  dochord  34908  dochsat  34921  dochshpncl  34922  dochsatshpb  34990  dochshpsat  34992  mapdval4N  35170  mapdsn  35179  hdmap14lem12  35420  hdmapip0  35456  hlhillcs  35499
  Copyright terms: Public domain W3C validator