Theorem iman 237

Description: Express implication in terms of conjunction. Theorem 3.4(27) of [Stoll] p. 176.

Assertion

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

Proof of Theorem iman

Step	Hyp	Ref	Expression
1		pm4.13 161	. . 3 |- (ps <-> -. -. ps)
2	1	imbi2i 185	. 2 |- ((ph -> ps) <-> (ph -> -. -. ps))
3		df-an 225	. . 3 |- ((ph /\ -. ps) <-> -. (ph -> -. -. ps))
4	3	con2bii 221	. 2 |- ((ph -> -. -. ps) <-> -. (ph /\ -. ps))
5	2, 4	bitr 173	1 |- ((ph -> ps) <-> -. (ph /\ -. ps))

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

This theorem is referenced by:  annim 238  pm3.37 286  pm4.14 352  dfbi 669  nicodraw 951  nicodmpraw 952  exanali 1042  dfpss3 2131  difdif 2163  dfss4 2239  ssdif0 2324  difin0ss 2329  inssdif0 2330  dfif2 2360  notzfaus 2737  inf3lem3 4598  nominpos 6000  cvbr2t 10166  cvnbtwn2t 10170  cvnbtwn3t 10171  cvnbtwn4t 10172  chpssat 10246  chrelat2 10248  chrelat3t 10254

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