Theorem annim 441

Description: Express conjunction in terms of implication. (Contributed by NM, 2-Aug-1994.)

Assertion

Ref	Expression
annim	|- ( ( ph /\ -. ps ) <-> -. ( ph -> ps ) )

Proof of Theorem annim

Step	Hyp	Ref	Expression
1		iman 440	. 2 |- ( ( ph -> ps ) <-> -. ( ph /\ -. ps ) )
2	1	con2bii 347	1 |- ( ( ph /\ -. ps ) <-> -. ( ph -> ps ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  pm4.61  442  pm4.52  512  xordi  937  dfifp6  1018  exanali  1786  sbn  2391  r19.35  3084  difin0ss  3946  ordsssuc2  5814  tfindsg  7060  findsg  7093  isf34lem4  9199  hashfun  13224  isprm5  15419  mdetunilem8  20425  4cycl2vnunb  27154  strlem6  29115  hstrlem6  29123  axacprim  31584  ceqsralv2  31607  dfrdg4  32058  andnand1  32398  relowlpssretop  33212  poimirlem1  33410  poimir  33442  2exanali  38587  limsupre2lem  39956  aifftbifffaibif  41088