Theorem iman 424

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

Proof of Theorem iman

Step	Hyp	Ref	Expression
1		notnot 291	. . 3
2	1	imbi2i 312	. 2
3		imnan 422	. 2
4	2, 3	bitri 249	1

Syntax hints:  -.wn 3  ->wi 4  <->wb 184  /\wa 369

This theorem is referenced by:  annim  425  pm3.24  882  xor  891  nannanOLD  1349  nic-mpALT  1505  nic-axALT  1507  rexanali  2910  difdif  3629  dfss4  3731  difin  3734  npss0  3865  ssdif0  3885  difin0ss  3894  inssdif0  3895  dfif2  3943  notzfaus  4627  dffv2  5946  tfinds  6694  domtriord  7683  inf3lem3  8068  nominpos  10800  isprm3  14226  vdwlem13  14511  vdwnn  14516  psgnunilem4  16522  efgredlem  16765  efgred  16766  ufinffr  20430  ptcmplem5  20556  nmoleub2lem2  21599  ellogdm  23020  pntpbnd  23773  cvbr2  27202  cvnbtwn2  27206  cvnbtwn3  27207  cvnbtwn4  27208  chpssati  27282  chrelat2i  27284  chrelat3  27290  df3nandALT1  29862  imnand2  29865  fdc  30238  bnj1476  33905  bnj110  33916  bnj1388  34089  bj-andnotim  34177  lpssat  34738  lssat  34741  lcvbr2  34747  lcvbr3  34748  lcvnbtwn2  34752  lcvnbtwn3  34753  cvrval2  34999  cvrnbtwn2  35000  cvrnbtwn3  35001  cvrnbtwn4  35004  atlrelat1  35046  hlrelat2  35127  dihglblem6  37067

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 185  df-an 371