Theorem impbida 877

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

Step	Hyp	Ref	Expression
1		impbida.1	. . 3 |- ( ( ph /\ ps ) -> ch )
2	1	ex 450	. 2 |- ( ph -> ( ps -> ch ) )
3		impbida.2	. . 3 |- ( ( ph /\ ch ) -> ps )
4	3	ex 450	. 2 |- ( ph -> ( ch -> ps ) )
5	2, 4	impbid 202	1 |- ( ph -> ( ps <-> ch ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  eqrdav  2621  frsn  5189  elsnxpOLD  5678  funfvbrb  6330  iinpreima  6345  frnssb  6391  fnprb  6472  fntpb  6473  fpr2g  6475  nvocnv  6537  fsnex  6538  f1prex  6539  f1ocnv2d  6886  el2xptp0  7212  1stconst  7265  2ndconst  7266  cnvf1o  7276  tfrlem15  7488  oeeui  7682  ersymb  7756  swoer  7772  erth  7791  boxriin  7950  boxcutc  7951  domunsncan  8060  pw2f1olem  8064  enen1  8100  enen2  8101  domen1  8102  domen2  8103  sdomen1  8104  sdomen2  8105  xpmapenlem  8127  ordiso2  8420  wdomen1  8481  wdomen2  8482  fin23lem26  9147  fpwwe2lem8  9459  r1wunlim  9559  mul2lt0bi  11936  ixxun  12191  xov1plusxeqvd  12318  fzsplit2  12366  fseq1p1m1  12414  elfz2nn0  12431  flflp1  12608  modsubdir  12739  zesq  12987  hashprg  13182  hashprgOLD  13183  hashgt0elexb  13190  hashbclem  13236  hashge2el2difb  13264  rereb  13860  rlimclim  14277  iserex  14387  caucvgb  14410  mptfzshft  14510  fsumrev  14511  climcnds  14583  fprodrev  14707  dvdsadd2b  15028  nn0ob  15100  bitsfzo  15157  dfgcd2  15263  dvdsmulgcd  15274  lcmgcdeq  15325  qden1elz  15465  mrcidb  16275  mrieqvlemd  16289  isacs2  16314  cicer  16466  ssclem  16479  issubc3  16509  ffthiso  16589  fuciso  16635  setcmon  16737  setcepi  16738  setcinv  16740  catciso  16757  acsfiindd  17177  issstrmgm  17252  issubmnd  17318  mhmf1o  17345  subsubm  17357  resmhm2b  17361  grpinvid1  17470  grpinvid2  17471  subsubg  17617  ssnmz  17636  ghmf1  17689  ghmf1o  17690  conjnmzb  17695  subggim  17708  gicsubgen  17721  gass  17734  odf1  17979  gex1  18006  fislw  18040  sylow3lem2  18043  sylow3lem6  18047  lsmdisj2a  18100  lsmdisj2b  18101  efgred2  18166  dmdprdsplit  18446  0unit  18680  irrednegb  18711  rhmf1o  18732  kerf1hrm  18743  isdrng2  18757  subrgunit  18798  issubdrg  18805  subsubrg  18806  islss3  18959  islss4  18962  lspsnel6  18994  lspsneq0b  19013  islmhm2  19038  lmhmf1o  19046  reslmhm2b  19054  lssvs0or  19110  lvecinv  19113  lspsnel4  19124  lspdisjb  19126  islbs2  19154  islbs3  19155  issubassa  19324  issubassa2  19345  gsumbagdiag  19376  subrgasclcl  19499  prmirredlem  19841  islindf3  20165  lindsmm  20167  lsslindf  20169  lsslinds  20170  matunit  20484  slesolinvbi  20487  en2top  20789  elcls  20877  neindisj2  20927  neiptopnei  20936  neiptopreu  20937  maxlp  20951  neitr  20984  iscncl  21073  cncnp  21084  isreg2  21181  dis2ndc  21263  1stccnp  21265  islly2  21287  dislly  21300  dissnlocfin  21332  kgencmp2  21349  pt1hmeo  21609  xkocnv  21617  t0kq  21621  uffixfr  21727  flimcf  21786  cnpflf2  21804  fclscf  21829  cnextf  21870  utopsnneiplem  22051  isucn2  22083  cfilucfil  22364  psmetutop  22372  restmetu  22375  tngngp2  22456  tngngp  22458  nmoleub  22535  metdseq0  22657  cnheibor  22754  pcophtb  22829  nmoleub2lem  22914  lmmbr  23056  iscfil3  23071  cmetss  23113  cldcss  23212  mbfeqalem  23409  mbfposb  23420  itg2const2  23508  itgss3  23581  plyco0  23948  dgrlt  24022  ulm2  24139  coseq00topi  24254  coseq0negpitopi  24255  sineq0  24273  relogbcxpb  24525  atans2  24658  xrlimcnp  24695  dchrelbas2  24962  dchrn0  24975  2sqb  25157  istrkg2ld  25359  tgcgreqb  25376  tgbtwncomb  25384  trgcgrg  25410  legov  25480  legov2  25481  legov3  25493  hlbtwn  25506  tglineelsb2  25527  tglinecom  25530  colline  25544  mirinv  25561  mirbtwnb  25567  mirbtwnhl  25575  perpcom  25608  isperp2  25610  oppcom  25636  opphllem3  25641  lnopp2hpgb  25655  colopp  25661  colhp  25662  lmieu  25676  iscgra1  25702  dfcgra2  25721  edgnbusgreu  26269  nb3grprlem1  26282  lfgriswlk  26585  eleclclwwlksnlem2  26939  clwwlksnscsh  26940  numclwwlk2lem1  27235  grpoinvid1  27382  grpoinvid2  27383  leopmul  28993  hst1h  29086  disjabrex  29395  disjabrexf  29396  erbr3b  29427  f1o3d  29431  funimass4f  29437  fgreu  29471  fcnvgreu  29472  1stpreimas  29483  fcobij  29500  resf1o  29505  fzsplit3  29553  eliccioo  29639  ogrpinv0le  29716  ogrpaddltbi  29719  ogrpaddltrbid  29721  ogrpinv0lt  29723  isarchi3  29741  1smat1  29870  fimaproj  29900  qtophaus  29903  reff  29906  locfinreflem  29907  cmpcref  29917  metider  29937  pstmfval  29939  qqhval2  30026  aean  30307  imambfm  30324  eulerpartlemgvv  30438  orvcgteel  30529  orvclteel  30534  ballotlemsf1o  30575  sgn3da  30603  sgnnbi  30607  sgnpbi  30608  sgnmulsgn  30611  sgnmulsgp  30612  actfunsnf1o  30682  reprsuc  30693  reprpmtf1o  30704  sconnpi1  31221  nosupbnd2  31862  slerec  31923  brofs2  32184  brifs2  32185  broutsideof2  32229  ltflcei  33397  poimirlem25  33434  ismblfin  33450  cnambfre  33458  ftc1anclem6  33490  ismndo1  33672  isdrngo2  33757  lshpnelb  34271  lshpnel2N  34272  lsatspn0  34287  lsatelbN  34293  lsat0cv  34320  lcvexch  34326  lcv1  34328  lkrshp3  34393  lkrpssN  34450  lkrss2N  34456  cvlsupr2  34630  atcvrlln  34806  llncvrlpln  34844  2llnmj  34846  lplncvrlvol  34902  2lplnmj  34908  polcon2bN  35206  pcl0bN  35209  lhpmcvr3  35311  lhpmatb  35317  ltrncoidN  35414  ltrneq3  35495  ltrniotavalbN  35872  cdlemg1cN  35875  diclspsn  36483  dihopelvalcpre  36537  dihord4  36547  dihord  36553  dihmeetlem4preN  36595  dih1dimatlem0  36617  dochsscl  36657  dochoccl  36658  dochord  36659  dochsat  36672  dochshpncl  36673  dochsatshpb  36741  dochshpsat  36743  mapdval4N  36921  mapdsn  36930  hdmap14lem12  37171  hdmapip0  37207  hlhillcs  37250  mrefg2  37270  mzpmfp  37310  lzenom  37333  elpell14qr2  37426  elpell1qr2  37436  pellfund14b  37463  congabseq  37541  acongeq  37550  jm2.23  37563  jm2.20nn  37564  jm2.25lem1  37565  wepwsolem  37612  islssfg2  37641  lnmlmic  37658  dfacbasgrp  37678  rfovcnvf1od  38298  dssmapnvod  38314  ntrclscls00  38364  rfcnpre3  39192  rfcnpre4  39193  rnmptssbi  39477  infxrgelbrnmpt  39683  xnegre  39696  ioossioobi  39743  iccshift  39744  iocopn  39746  eliccelioc  39747  iooshift  39748  icoopn  39751  qinioo  39762  limcdm0  39850  islptre  39851  islpcn  39871  limcresioolb  39875  climuzlem  39975  climlimsup  39992  liminfgelimsup  40014  liminfgelimsupuz  40020  climliminf  40038  climliminflimsup  40040  climliminflimsup2  40041  xlimbr  40053  xlimmnfv  40060  xlimpnfv  40064  xlimclim2  40066  dfxlim2v  40073  fperdvper  40133  itgperiod  40197  fourierdlem32  40356  fourierdlem33  40357  fourierdlem48  40371  fourierdlem49  40372  fourierdlem71  40394  fourierdlem81  40404  smfliminflem  41036  smfliminfmpt  41038  m1mod0mod1  41339  mgmhmf1o  41787  issubmgm2  41790  subsubmgm  41797  resmgmhm2b  41800  rnghmf1o  41903  rngcinv  41981  rngcinvALTV  41993  ringcinv  42032  ringcinvALTV  42056