Theorem imnan 422

Description: Express implication in terms of conjunction. (Contributed by NM, 9-Apr-1994.)

Assertion

Ref	Expression
imnan

Proof of Theorem imnan

Step	Hyp	Ref	Expression
1		df-an 371	. 2
2	1	con2bii 332	1

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

This theorem is referenced by:  imnani  423  iman  424  ianor  488  nan  580  pm5.17  888  pm5.16  890  dn1  966  nannan  1348  nic-ax  1506  nic-axALT  1507  alinexa  1663  dfsb3  2115  ralinexa  2909  pssn2lp  3604  disj  3867  minel  3882  disjsn  4090  sotric  4831  ordtri1  4916  poirr2  5396  funun  5635  imadif  5668  brprcneu  5864  soisoi  6224  ordsucss  6653  ordunisuc2  6679  oalimcl  7228  omlimcl  7246  unblem1  7792  suppr  7950  cantnfp1lem3  8120  cantnfp1lem3OLD  8146  alephnbtwn  8473  kmlem4  8554  cfsuc  8658  isf32lem5  8758  hargch  9072  xrltnsym2  11373  fzp1nel  11791  fsumsplit  13562  sumsplit  13583  phiprmpw  14306  odzdvds  14322  pcdvdsb  14392  prmreclem5  14438  ramlb  14537  pltn2lp  15599  gsumzsplit  16944  gsumzsplitOLD  16945  dprdcntz2  17086  lbsextlem4  17807  obselocv  18759  maducoeval2  19142  lmmo  19881  kqcldsat  20234  rnelfmlem  20453  tsmssplit  20654  itg2splitlem  22155  itg2split  22156  fsumharmonic  23341  lgsne0  23608  lgsquadlem3  23631  nmounbi  25691  hatomistici  27281  eliccelico  27588  elicoelioo  27589  nn0min  27611  2sqcoprm  27635  isarchi2  27729  archiabl  27742  oddpwdc  28293  eulerpartlemsv2  28297  eulerpartlems  28299  eulerpartlemv  28303  eulerpartlemgh  28317  eulerpartlemgs2  28319  ballotlem2  28427  ballotlemfrcn0  28468  subfacp1lem6  28629  poseq  29333  wzel  29380  nodenselem5  29445  nodenselem7  29447  nocvxminlem  29450  nofulllem5  29466  df3nandALT1  29862  df3nandALT2  29863  limsucncmpi  29910  nninfnub  30244  n0el  30600  fnwe2lem2  30997  pm10.57  31276  limclner  31657  icccncfext  31690  stoweidlem14  31796  stoweidlem34  31816  stoweidlem44  31826  ldepslinc  33110  alimp-no-surprise  33196  bnj1533  33910  bnj1204  34068  bnj1280  34076  atlatmstc  35044  dfxor4  37789

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