Theorem iman 440

Description: Express implication in terms of conjunction. Theorem 3.4(27) of [Stoll] p. 176. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 30-Oct-2012.)

Assertion

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

Proof of Theorem iman

Step	Hyp	Ref	Expression
1		notnotb 304	. . 3 |- ( ps <-> -. -. ps )
2	1	imbi2i 326	. 2 |- ( ( ph -> ps ) <-> ( ph -> -. -. ps ) )
3		imnan 438	. 2 |- ( ( ph -> -. -. ps ) <-> -. ( ph /\ -. ps ) )
4	2, 3	bitri 264	1 |- ( ( ph -> ps ) <-> -. ( ph /\ -. ps ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  annim  441  pm3.24  926  xor  935  nic-mpALT  1597  nic-axALT  1599  rexanali  2998  difdif  3736  dfss4  3858  difin  3861  ssdif0  3942  difin0ss  3946  inssdif0  3947  npss0OLD  4015  dfif2  4088  notzfaus  4840  dffv2  6271  tfinds  7059  domtriord  8106  inf3lem3  8527  nominpos  11269  isprm3  15396  vdwlem13  15697  vdwnn  15702  psgnunilem4  17917  efgredlem  18160  efgred  18161  ufinffr  21733  ptcmplem5  21860  nmoleub2lem2  22916  ellogdm  24385  pntpbnd  25277  cvbr2  29142  cvnbtwn2  29146  cvnbtwn3  29147  cvnbtwn4  29148  chpssati  29222  chrelat2i  29224  chrelat3  29230  bnj1476  30917  bnj110  30928  bnj1388  31101  df3nandALT1  32396  imnand2  32399  bj-andnotim  32573  lindsenlbs  33404  poimirlem11  33420  poimirlem12  33421  fdc  33541  lpssat  34300  lssat  34303  lcvbr2  34309  lcvbr3  34310  lcvnbtwn2  34314  lcvnbtwn3  34315  cvrval2  34561  cvrnbtwn2  34562  cvrnbtwn3  34563  cvrnbtwn4  34566  atlrelat1  34608  hlrelat2  34689  dihglblem6  36629  or3or  38319  uneqsn  38321  plvcofphax  41114