Theorem impbida 604

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 115	. 2 |- ( ph -> ( ps -> ch ) )
3		impbida.2	. . 3 |- ( ( ph /\ ch ) -> ps )
4	3	ex 115	. 2 |- ( ph -> ( ch -> ps ) )
5	2, 4	impbid 129	1 |- ( ph -> ( ps <-> ch ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  biadanid  622  eqrdav  2237  funfvbrb  5825  f1ocnv2d  6297  f1o3d  6301  funimass4f  6363  1stconst  6461  2ndconst  6462  cnvf1o  6465  ersymb  6825  swoer  6839  erth  6857  pw2f1odclem  7138  enen1  7144  enen2  7145  domen1  7146  domen2  7147  xpmapenlem  7153  fidifsnen  7176  fundmfibi  7256  f1dmvrnfibi  7262  2omap  7324  2omapfi  7326  ordiso2  7381  omniwomnimkv  7513  enwomnilem  7515  nninfwlpoimlemginf  7522  pw1if  7590  exmidapne  7632  infregelbex  10014  fzsplit2  10472  fzsplit3  10475  fseq1p1m1  10518  elfz2nn0  10536  infssfzcldc  10686  infssfzledc  10687  btwnzge0  10756  modqsubdir  10851  zesq  11117  hashprg  11271  sseqn  11301  hashfibclem  11304  rereb  11650  abslt  11877  absle  11878  maxleastb  12003  maxltsup  12007  xrltmaxsup  12048  xrmaxltsup  12049  iserex  12130  mptfzshft  12234  fsumrev  12235  fprodrev  12411  dvdsadd2b  12632  nn0ob  12700  bitsfzo  12747  dfgcd3  12812  dfgcd2  12816  dvdsmulgcd  12827  lcmgcdeq  12886  isprm5  12946  nnmaxpwlemparts  12977  qden1elz  13010  ballotfilemsf1o  13315  issubmnd  13814  mhmf1o  13836  subsubm  13849  resmhm2b  13855  grpinvid1  13916  grpinvid2  13917  subsubg  14059  ssnmz  14073  ghmf1  14135  kerf1ghm  14136  ghmf1o  14137  conjnmzb  14142  0unit  14545  rhmf1o  14584  subsubrng  14631  subrgunit  14656  subsubrg  14662  ringunitap  14702  drngunitap  14717  islss3  14825  islss4  14828  ellspsn6  14854  lspsneq0b  14873  dflidl2rng  14927  issubassa  15122  issubassa2  15144  psrbaglefifi  15172  gsumbagdiagfi  15176  cncnp  15456  xmetxpbl  15734  dedekindicc  15859  coseq0q4123  16061  coseq0negpitopi  16063  relogeftb  16094  relogbcxpbap  16201  upgr2wlkdc  16823  pw1map  17230  pwf1oexmid  17234  isomninnlem  17285  apdiff  17304  iswomninnlem  17306  ismkvnnlem  17309  redcwlpolemeq1  17311