Theorem annim 415

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 414	. 2 |- ( ( ph -> ps ) <-> -. ( ph /\ -. ps ) )
2	1	con2bii 323	1 |- ( ( ph /\ -. ps ) <-> -. ( ph -> ps ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 177   /\ wa 359

This theorem is referenced by:  pm4.61  416  pm4.52  478  xordi  866  exanali  1592  19.35  1607  rexanali  2712  r19.35  2815  difin0ss  3654  ordsssuc2  4629  tfindsg  4799  findsg  4831  isf34lem4  8213  hashfun  11655  isprm5  13067  strlem6  23712  hstrlem6  23720  axacprim  25109  dfrdg4  25703  andnand1  26052  2exanali  27454  4cycl2vnunb  28121

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

This theorem depends on definitions:  df-bi 178  df-an 361