Theorem imnan 404

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 401	. 2 ⊢ ((𝜑 ∧ 𝜓) ↔ ¬ (𝜑 → ¬ 𝜓))
2	1	con2bii 360	1 ⊢ ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  imnani  405  iman  406  mpnanrd  414  nan  842  ianor  997  pm5.17  1027  pm5.16  1029  dn1  1071  dfnan2  1521  nic-ax  1700  nic-axALT  1701  imnang  1869  dfsb3  2532  ralinexa  3124  pssn2lp  4067  indifdi  4255  disj  4416  disjsn  4682  sotric  5600  poirr2  6125  ordtri1  6395  funun  6583  imadif  6621  brprcneu  6872  brprcneuALT  6873  soisoi  7327  ordsucss  7814  ordunisuc2  7840  poseq  8154  oalimcl  8545  omlimcl  8563  unblem1  9252  suppr  9432  infpr  9465  nelaneqOLD  9565  cantnfp1lem3  9649  alephnbtwn  10055  kmlem4  10137  cfsuc  10241  isf32lem5  10341  hargch  10658  xrltnsym2  13163  fzp1nel  13639  fsumsplit  15792  sumsplit  15819  phiprmpw  16835  odzdvds  16855  pcdvdsb  16929  prmreclem5  16980  ramlb  17079  pltn2lp  18395  gsumzsplit  19997  dprdcntz2  20110  lbsextlem4  21263  obselocv  21847  psdmul  22298  maducoeval2  22766  lmmo  23506  kqcldsat  23859  rnelfmlem  24078  tsmssplit  24278  itg2splitlem  25876  itg2split  25877  fsumharmonic  27142  lgsne0  27465  lgsquadlem3  27512  2sqcoprm  27565  nosepssdm  27816  nosupbnd1lem4  27841  noinfbnd1lem4  27856  nocvxminlem  27913  bdayfinbndlem1  28626  axtgupdim2  28706  nmounbi  31069  hatomistici  32655  eliccelico  33063  elicoelioo  33064  nn0difffzod  33090  nn0min  33106  isarchi2  33446  archiabl  33459  extdgfialglem1  34027  oddpwdc  34689  eulerpartlemsv2  34693  eulerpartlems  34695  eulerpartlemv  34699  eulerpartlemgh  34713  eulerpartlemgs2  34715  ballotlemfrcn0  34865  bnj1533  35185  bnj1204  35345  bnj1280  35353  xoromon  35422  fineqvinfep  35461  subfacp1lem6  35576  wzel  36213  df3nandALT1  36799  df3nandALT2  36800  limsucncmpi  36845  weiunfr  36867  regsfromregtco  36938  unblimceq0  36985  bj-axseprep  37599  relowlpssretop  37898  pibt2  37951  nninfnub  38290  atlatmstc  39983  fnwe2lem2  43670  dfxor4  44384  pm10.57  44973  limclner  46257  limsupub  46310  limsuppnflem  46316  limsupre2lem  46330  icccncfext  46493  stoweidlem14  46620  stoweidlem34  46640  stoweidlem44  46650  ldepslinc  49174  fdomne0  49513  map0cor  49518  elsetrecslem  50362  alimp-no-surprise  50444