Theorem impbida 596

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  614  eqrdav  2192  funfvbrb  5671  f1ocnv2d  6122  1stconst  6274  2ndconst  6275  cnvf1o  6278  ersymb  6601  swoer  6615  erth  6633  pw2f1odclem  6890  enen1  6896  enen2  6897  domen1  6898  domen2  6899  xpmapenlem  6905  fidifsnen  6926  fundmfibi  6997  f1dmvrnfibi  7003  ordiso2  7094  omniwomnimkv  7226  enwomnilem  7228  nninfwlpoimlemginf  7235  exmidapne  7320  infregelbex  9663  fzsplit2  10116  fseq1p1m1  10160  elfz2nn0  10178  btwnzge0  10369  modqsubdir  10464  zesq  10729  hashprg  10879  rereb  11007  abslt  11232  absle  11233  maxleastb  11358  maxltsup  11362  xrltmaxsup  11400  xrmaxltsup  11401  iserex  11482  mptfzshft  11585  fsumrev  11586  fprodrev  11762  dvdsadd2b  11983  nn0ob  12049  dfgcd3  12147  dfgcd2  12151  dvdsmulgcd  12162  lcmgcdeq  12221  isprm5  12280  qden1elz  12343  issubmnd  13023  mhmf1o  13042  subsubm  13055  resmhm2b  13061  grpinvid1  13124  grpinvid2  13125  subsubg  13267  ssnmz  13281  ghmf1  13343  kerf1ghm  13344  ghmf1o  13345  conjnmzb  13350  0unit  13625  rhmf1o  13664  subsubrng  13710  subrgunit  13735  subsubrg  13741  islss3  13875  islss4  13878  lspsnel6  13904  lspsneq0b  13923  dflidl2rng  13977  cncnp  14398  xmetxpbl  14676  dedekindicc  14787  coseq0q4123  14969  coseq0negpitopi  14971  relogeftb  15000  relogbcxpbap  15097  pwf1oexmid  15490  isomninnlem  15520  apdiff  15538  iswomninnlem  15539  ismkvnnlem  15542  redcwlpolemeq1  15544