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  488  xordi  883  exanali  1637  19.35  1654  sbn  2080  rexanali  2751  r19.35  2857  difin0ss  3733  ordsssuc2  4794  tfindsg  6460  findsg  6492  isf34lem4  8534  hashfun  12182  isprm5  13780  mdetunilem8  18266  strlem6  25482  hstrlem6  25490  archiabl  26038  ordtconlem1  26207  axacprim  27204  dfrdg4  27827  andnand1  28091  2exanali  29482  4cycl2vnunb  30452