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  2195  funfvbrb  5675  f1ocnv2d  6127  1stconst  6279  2ndconst  6280  cnvf1o  6283  ersymb  6606  swoer  6620  erth  6638  pw2f1odclem  6895  enen1  6901  enen2  6902  domen1  6903  domen2  6904  xpmapenlem  6910  fidifsnen  6931  fundmfibi  7004  f1dmvrnfibi  7010  ordiso2  7101  omniwomnimkv  7233  enwomnilem  7235  nninfwlpoimlemginf  7242  exmidapne  7327  infregelbex  9672  fzsplit2  10125  fseq1p1m1  10169  elfz2nn0  10187  btwnzge0  10390  modqsubdir  10485  zesq  10750  hashprg  10900  rereb  11028  abslt  11253  absle  11254  maxleastb  11379  maxltsup  11383  xrltmaxsup  11422  xrmaxltsup  11423  iserex  11504  mptfzshft  11607  fsumrev  11608  fprodrev  11784  dvdsadd2b  12005  nn0ob  12073  bitsfzo  12119  dfgcd3  12177  dfgcd2  12181  dvdsmulgcd  12192  lcmgcdeq  12251  isprm5  12310  qden1elz  12373  issubmnd  13083  mhmf1o  13102  subsubm  13115  resmhm2b  13121  grpinvid1  13184  grpinvid2  13185  subsubg  13327  ssnmz  13341  ghmf1  13403  kerf1ghm  13404  ghmf1o  13405  conjnmzb  13410  0unit  13685  rhmf1o  13724  subsubrng  13770  subrgunit  13795  subsubrg  13801  islss3  13935  islss4  13938  lspsnel6  13964  lspsneq0b  13983  dflidl2rng  14037  cncnp  14466  xmetxpbl  14744  dedekindicc  14869  coseq0q4123  15070  coseq0negpitopi  15072  relogeftb  15101  relogbcxpbap  15201  pwf1oexmid  15644  isomninnlem  15674  apdiff  15692  iswomninnlem  15693  ismkvnnlem  15696  redcwlpolemeq1  15698