Theorem iman 256

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		notnot 178	. . 3 |- (ps <-> -. -. ps)
2	1	imbi2i 202	. 2 |- ((ph -> ps) <-> (ph -> -. -. ps))
3		df-an 242	. . 3 |- ((ph /\ -. ps) <-> -. (ph -> -. -. ps))
4	3	con2bii 238	. 2 |- ((ph -> -. -. ps) <-> -. (ph /\ -. ps))
5	2, 4	bitri 190	1 |- ((ph -> ps) <-> -. (ph /\ -. ps))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   /\ wa 240

This theorem is referenced by:  annim 257  pm3.37 308  pm4.14 379  dfbi3 733  nic-justlem 1231  nic-mpALT 1238  nic-axALT 1240  exanali 1390  dfpss3OLD 2696  difdif 2734  dfss4 2827  dfss4OLD 2828  difin 2831  npss0 2911  ssdif0 2934  difin0ss 2939  inssdif0 2940  inssdif0OLD 2941  dfif2 2984  notzfaus 3478  tfinds 3942  dffv2 4734  domtriord 5546  ordiso 5683  ordtypelem7 5690  inf3lem3 5721  nominpos 7230  cvbr2 11855  cvnbtwn2 11859  cvnbtwn3 11860  cvnbtwn4 11861  chpssati 11935  chrelat2i 11937  chrelat3 11943  bnj52 12427  bnj112 12457  bnj1477 13153  mulgcdlem2 13757  isprm3 13776  df3nandALT1 14146  imnand2 14149  dmsdtriordOLD 15360  ordisoOLD 15374  ordtypelem7OLD 15381  locfincomp 15514  ufinffr 15578  fdc 15812  prtlem80 16247  cvrval2 16991  cvrnbtwn2 16992  cvrnbtwn3 16993  cvrnbtwn4 16996  hlrelat1 17049  hlrelat2 17052

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 164  df-an 242

Copyright terms: Public domain