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  1494  nic-ax  1673  nic-axALT  1674  imnang  1842  dfsb3  2492  ralinexa  3082  pssn2lp  4055  indifdi  4245  disj  4401  disjsn  4663  sotric  5557  poirr2  6073  ordtri1  6340  funun  6528  imadif  6566  brprcneu  6812  brprcneuALT  6813  soisoi  7265  ordsucss  7751  ordunisuc2  7777  poseq  8091  oalimcl  8478  omlimcl  8496  unblem1  9181  suppr  9362  infpr  9395  nelaneq  9493  cantnfp1lem3  9576  alephnbtwn  9965  kmlem4  10048  cfsuc  10151  isf32lem5  10251  hargch  10567  xrltnsym2  13040  fzp1nel  13514  fsumsplit  15648  sumsplit  15675  phiprmpw  16687  odzdvds  16707  pcdvdsb  16781  prmreclem5  16832  ramlb  16931  pltn2lp  18245  gsumzsplit  19806  dprdcntz2  19919  lbsextlem4  21068  obselocv  21635  psdmul  22051  maducoeval2  22525  lmmo  23265  kqcldsat  23618  rnelfmlem  23837  tsmssplit  24037  itg2splitlem  25647  itg2split  25648  fsumharmonic  26920  lgsne0  27244  lgsquadlem3  27291  2sqcoprm  27344  nosepssdm  27596  nosupbnd1lem4  27621  noinfbnd1lem4  27636  nocvxminlem  27688  axtgupdim2  28416  nmounbi  30720  hatomistici  32306  eliccelico  32721  elicoelioo  32722  nn0difffzod  32750  nn0min  32766  isarchi2  33128  archiabl  33141  extdgfialglem1  33665  oddpwdc  34328  eulerpartlemsv2  34332  eulerpartlems  34334  eulerpartlemv  34338  eulerpartlemgh  34352  eulerpartlemgs2  34354  ballotlemfrcn0  34504  bnj1533  34825  bnj1204  34985  bnj1280  34993  subfacp1lem6  35168  wzel  35808  df3nandALT1  36383  df3nandALT2  36384  limsucncmpi  36429  weiunfr  36451  unblimceq0  36491  relowlpssretop  37348  pibt2  37401  nninfnub  37741  atlatmstc  39308  fnwe2lem2  43034  dfxor4  43749  pm10.57  44354  limclner  45642  limsupub  45695  limsuppnflem  45701  limsupre2lem  45715  icccncfext  45878  stoweidlem14  46005  stoweidlem34  46025  stoweidlem44  46035  ldepslinc  48504  fdomne0  48844  map0cor  48849  elsetrecslem  49694  alimp-no-surprise  49776