Theorem annim 238

Description: Express conjunction in terms of implication.

Assertion

Ref	Expression
annim	|- ((ph /\ -. ps) <-> -. (ph -> ps))

Proof of Theorem annim

Step	Hyp	Ref	Expression
1		iman 237	. 2 |- ((ph -> ps) <-> -. (ph /\ -. ps))
2	1	con2bii 221	1 |- ((ph /\ -. ps) <-> -. (ph -> ps))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 146   /\ wa 223

This theorem is referenced by:  pm4.61 239  pm4.78 354  pm5.18 659  19.35 1073  a12studyALT 1377  rexanali 1681  r19.35 1756  nss 2109  difin0ss 2328  nssss 2759  findsg 3152  tfindsg 3157  climubi 7097  strlem6 10121  hstrlem6 10129

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain