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 950  nicodmpraw 951  exanali 1041  dfpss3 2130  difdif 2162  dfss4 2238  ssdif0 2323  difin0ss 2328  inssdif0 2329  dfif2 2359  notzfaus 2736  inf3lem3 4595  nominpos 5998  cvbr2t 10148  cvnbtwn2t 10152  cvnbtwn3t 10153  cvnbtwn4t 10154  chpssat 10227  chrelat2 10229  chrelat3t 10235

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