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 660  19.35 1075  a12studyALT 1379  rexanali 1684  r19.35 1759  nss 2113  difin0ss 2332  nssss 2764  findsg 3157  tfindsg 3162  climubi 7153  strlem6 10183  hstrlem6 10191

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