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  2233  funfvbrb  5793  f1ocnv2d  6261  1stconst  6419  2ndconst  6420  cnvf1o  6423  ersymb  6783  swoer  6797  erth  6815  pw2f1odclem  7089  enen1  7095  enen2  7096  domen1  7097  domen2  7098  xpmapenlem  7104  fidifsnen  7127  fundmfibi  7207  f1dmvrnfibi  7213  2omap  7271  2omapfi  7273  ordiso2  7328  omniwomnimkv  7460  enwomnilem  7462  nninfwlpoimlemginf  7469  pw1if  7537  exmidapne  7576  infregelbex  9933  fzsplit2  10387  fseq1p1m1  10432  elfz2nn0  10450  btwnzge0  10664  modqsubdir  10759  zesq  11024  hashprg  11177  sseqn  11207  hashfibclem  11210  rereb  11552  abslt  11777  absle  11778  maxleastb  11903  maxltsup  11907  xrltmaxsup  11946  xrmaxltsup  11947  iserex  12028  mptfzshft  12132  fsumrev  12133  fprodrev  12309  dvdsadd2b  12530  nn0ob  12598  bitsfzo  12645  dfgcd3  12710  dfgcd2  12714  dvdsmulgcd  12725  lcmgcdeq  12784  isprm5  12843  qden1elz  12906  issubmnd  13672  mhmf1o  13700  subsubm  13713  resmhm2b  13719  grpinvid1  13782  grpinvid2  13783  subsubg  13931  ssnmz  13945  ghmf1  14007  kerf1ghm  14008  ghmf1o  14009  conjnmzb  14014  0unit  14291  rhmf1o  14330  subsubrng  14376  subrgunit  14401  subsubrg  14407  islss3  14544  islss4  14547  lspsnel6  14573  lspsneq0b  14592  dflidl2rng  14646  cncnp  15112  xmetxpbl  15390  dedekindicc  15515  coseq0q4123  15716  coseq0negpitopi  15718  relogeftb  15747  relogbcxpbap  15847  upgr2wlkdc  16389  pw1map  16786  pwf1oexmid  16790  isomninnlem  16831  apdiff  16849  iswomninnlem  16851  ismkvnnlem  16854  redcwlpolemeq1  16856