Theorem impbida 600

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 ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  biadanid  618  eqrdav  2230  funfvbrb  5769  f1ocnv2d  6237  1stconst  6395  2ndconst  6396  cnvf1o  6399  ersymb  6759  swoer  6773  erth  6791  pw2f1odclem  7063  enen1  7069  enen2  7070  domen1  7071  domen2  7072  xpmapenlem  7078  fidifsnen  7100  fundmfibi  7180  f1dmvrnfibi  7186  ordiso2  7294  omniwomnimkv  7426  enwomnilem  7428  nninfwlpoimlemginf  7435  pw1if  7503  exmidapne  7539  infregelbex  9893  fzsplit2  10347  fseq1p1m1  10391  elfz2nn0  10409  btwnzge0  10623  modqsubdir  10718  zesq  10983  hashprg  11135  rereb  11503  abslt  11728  absle  11729  maxleastb  11854  maxltsup  11858  xrltmaxsup  11897  xrmaxltsup  11898  iserex  11979  mptfzshft  12083  fsumrev  12084  fprodrev  12260  dvdsadd2b  12481  nn0ob  12549  bitsfzo  12596  dfgcd3  12661  dfgcd2  12665  dvdsmulgcd  12676  lcmgcdeq  12735  isprm5  12794  qden1elz  12857  issubmnd  13605  mhmf1o  13633  subsubm  13646  resmhm2b  13652  grpinvid1  13715  grpinvid2  13716  subsubg  13864  ssnmz  13878  ghmf1  13940  kerf1ghm  13941  ghmf1o  13942  conjnmzb  13947  0unit  14224  rhmf1o  14263  subsubrng  14309  subrgunit  14334  subsubrg  14340  islss3  14475  islss4  14478  lspsnel6  14504  lspsneq0b  14523  dflidl2rng  14577  cncnp  15041  xmetxpbl  15319  dedekindicc  15444  coseq0q4123  15645  coseq0negpitopi  15647  relogeftb  15676  relogbcxpbap  15776  upgr2wlkdc  16318  2omap  16715  pw1map  16717  pwf1oexmid  16721  isomninnlem  16762  apdiff  16780  iswomninnlem  16782  ismkvnnlem  16785  redcwlpolemeq1  16787