Theorem annim 423

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

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

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 369

This theorem is referenced by:  pm4.61  424  pm4.52  489  xordi  896  dfifp6  1392  exanali  1691  19.35OLD  1709  sbn  2156  rexanaliOLD  2912  r19.35  2954  difin0ss  3838  ordsssuc2  5498  tfindsg  6678  findsg  6711  isf34lem4  8789  hashfun  12544  isprm5  14462  mdetunilem8  19413  4cycl2vnunb  25434  strlem6  27588  hstrlem6  27596  axacprim  29908  dfrdg4  30289  andnand1  30631  relowlpssretop  31281  2exanali  36141