Theorem annim 425

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

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 369

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 185  df-an 371

This theorem is referenced by:  pm4.61  426  pm4.52  491  xordi  890  exanali  1638  19.35OLD  1656  sbn  2091  rexanali  2877  r19.35  2967  difin0ss  3848  ordsssuc2  4910  tfindsg  6576  findsg  6608  isf34lem4  8652  hashfun  12312  isprm5  13911  mdetunilem8  18552  strlem6  25807  hstrlem6  25815  archiabl  26355  ordtconlem1  26494  axacprim  27497  dfrdg4  28120  andnand1  28384  2exanali  29783  4cycl2vnunb  30752  bj-dfif6  32400