Theorem annim 426

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

Syntax hints:   -. wn 3   -> wi 4   <-> wb 187   /\ wa 370

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 188  df-an 372

This theorem is referenced by:  pm4.61  427  pm4.52  493  xordi  903  dfifp6  1426  exanali  1715  sbn  2189  rexanaliOLD  2930  r19.35  2972  difin0ss  3863  ordsssuc2  5530  tfindsg  6701  findsg  6734  isf34lem4  8814  hashfun  12613  isprm5  14650  mdetunilem8  19642  4cycl2vnunb  25743  strlem6  27907  hstrlem6  27915  axacprim  30342  dfrdg4  30723  andnand1  31064  relowlpssretop  31731  poimirlem1  31905  poimir  31937  2exanali  36707  aifftbifffaibif  38380