Theorem annim 431

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

Syntax hints:   -. wn 3   -> wi 4   <-> wb 189   /\ wa 375

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 190  df-an 377

This theorem is referenced by:  pm4.61  432  pm4.52  498  xordi  909  dfifp6  1434  exanali  1725  sbn  2221  r19.35  2905  difin0ss  3801  ordsssuc2  5490  tfindsg  6675  findsg  6708  isf34lem4  8794  hashfun  12604  isprm5  14662  mdetunilem8  19655  4cycl2vnunb  25757  strlem6  27921  hstrlem6  27929  axacprim  30340  ceqsralv2  30364  dfrdg4  30724  andnand1  31065  relowlpssretop  31769  poimirlem1  31943  poimir  31975  2exanali  36738  aifftbifffaibif  38600