Theorem imnan 399

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

Assertion

Ref	Expression
imnan	⊢ ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓))

Proof of Theorem imnan

Step	Hyp	Ref	Expression
1		df-an 396	. 2 ⊢ ((𝜑 ∧ 𝜓) ↔ ¬ (𝜑 → ¬ 𝜓))
2	1	con2bii 357	1 ⊢ ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  imnani  400  iman  401  mpnanrd  409  nan  829  ianor  983  pm5.17  1013  pm5.16  1015  dn1  1057  dfnan2  1495  nic-ax  1674  nic-axALT  1675  imnang  1843  dfsb3  2498  ralinexa  3089  pssn2lp  4056  indifdi  4246  disj  4402  disjsn  4668  sotric  5562  poirr2  6081  ordtri1  6350  funun  6538  imadif  6576  brprcneu  6824  brprcneuALT  6825  soisoi  7274  ordsucss  7760  ordunisuc2  7786  poseq  8100  oalimcl  8487  omlimcl  8505  unblem1  9192  suppr  9375  infpr  9408  nelaneq  9506  cantnfp1lem3  9589  alephnbtwn  9981  kmlem4  10064  cfsuc  10167  isf32lem5  10267  hargch  10584  xrltnsym2  13052  fzp1nel  13527  fsumsplit  15664  sumsplit  15691  phiprmpw  16703  odzdvds  16723  pcdvdsb  16797  prmreclem5  16848  ramlb  16947  pltn2lp  18262  gsumzsplit  19856  dprdcntz2  19969  lbsextlem4  21116  obselocv  21683  psdmul  22109  maducoeval2  22584  lmmo  23324  kqcldsat  23677  rnelfmlem  23896  tsmssplit  24096  itg2splitlem  25705  itg2split  25706  fsumharmonic  26978  lgsne0  27302  lgsquadlem3  27349  2sqcoprm  27402  nosepssdm  27654  nosupbnd1lem4  27679  noinfbnd1lem4  27694  nocvxminlem  27750  bdayfinbndlem1  28463  axtgupdim2  28543  nmounbi  30851  hatomistici  32437  eliccelico  32857  elicoelioo  32858  nn0difffzod  32884  nn0min  32901  isarchi2  33267  archiabl  33280  extdgfialglem1  33849  oddpwdc  34511  eulerpartlemsv2  34515  eulerpartlems  34517  eulerpartlemv  34521  eulerpartlemgh  34535  eulerpartlemgs2  34537  ballotlemfrcn0  34687  bnj1533  35008  bnj1204  35168  bnj1280  35176  xoromon  35245  fineqvinfep  35281  subfacp1lem6  35379  wzel  36016  df3nandALT1  36593  df3nandALT2  36594  limsucncmpi  36639  weiunfr  36661  regsfromregtr  36668  unblimceq0  36707  relowlpssretop  37569  pibt2  37622  nninfnub  37952  atlatmstc  39589  fnwe2lem2  43303  dfxor4  44017  pm10.57  44622  limclner  45905  limsupub  45958  limsuppnflem  45964  limsupre2lem  45978  icccncfext  46141  stoweidlem14  46268  stoweidlem34  46288  stoweidlem44  46298  ldepslinc  48765  fdomne0  49105  map0cor  49110  elsetrecslem  49954  alimp-no-surprise  50036