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  893  exanali  1647  19.35OLD  1665  sbn  2105  rexanaliOLD  2967  r19.35  3008  difin0ss  3893  ordsssuc2  4966  tfindsg  6673  findsg  6705  isf34lem4  8753  hashfun  12455  isprm5  14105  mdetunilem8  18885  4cycl2vnunb  24690  strlem6  26848  hstrlem6  26856  archiabl  27401  ordtconlem1  27539  axacprim  28551  dfrdg4  29174  andnand1  29438  2exanali  30871  limcrecl  31171  bj-dfif6  33231