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  dfbi3 672  nicodraw 954  nicodmpraw 955  exanali 1045  dfpss3 2137  difdif 2169  dfss4 2245  ssdif0 2331  difin0ss 2336  inssdif0 2337  dfif2 2367  notzfaus 2746  inf3lem3 4624  nominpos 6045  cvbr2t 10205  cvnbtwn2t 10209  cvnbtwn3t 10210  cvnbtwn4t 10211  chpssat 10285  chrelat2 10287  chrelat3t 10293

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