Theorem imnan 400

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  imnani  401  iman  402  mpnanrd  410  nan  835  ianor  989  pm5.17  1019  pm5.16  1021  dn1  1063  dfnan2  1501  nic-ax  1680  nic-axALT  1681  imnang  1849  dfsb3  2502  ralinexa  3092  pssn2lp  4035  indifdi  4222  disj  4378  disjsn  4643  sotric  5556  poirr2  6074  ordtri1  6343  funun  6531  imadif  6569  brprcneu  6817  brprcneuALT  6818  soisoi  7272  ordsucss  7758  ordunisuc2  7784  poseq  8098  oalimcl  8485  omlimcl  8503  unblem1  9192  suppr  9375  infpr  9408  nelaneqOLD  9508  cantnfp1lem3  9592  alephnbtwn  9984  kmlem4  10067  cfsuc  10170  isf32lem5  10270  hargch  10587  xrltnsym2  13080  fzp1nel  13556  fsumsplit  15694  sumsplit  15721  phiprmpw  16737  odzdvds  16757  pcdvdsb  16831  prmreclem5  16882  ramlb  16981  pltn2lp  18296  gsumzsplit  19893  dprdcntz2  20006  lbsextlem4  21154  obselocv  21703  psdmul  22154  maducoeval2  22623  lmmo  23363  kqcldsat  23716  rnelfmlem  23935  tsmssplit  24135  itg2splitlem  25733  itg2split  25734  fsumharmonic  26993  lgsne0  27316  lgsquadlem3  27363  2sqcoprm  27416  nosepssdm  27668  nosupbnd1lem4  27693  noinfbnd1lem4  27708  nocvxminlem  27764  bdayfinbndlem1  28477  axtgupdim2  28557  nmounbi  30865  hatomistici  32451  eliccelico  32869  elicoelioo  32870  nn0difffzod  32896  nn0min  32913  isarchi2  33266  archiabl  33279  extdgfialglem1  33876  oddpwdc  34538  eulerpartlemsv2  34542  eulerpartlems  34544  eulerpartlemv  34548  eulerpartlemgh  34562  eulerpartlemgs2  34564  ballotlemfrcn0  34714  bnj1533  35034  bnj1204  35194  bnj1280  35202  xoromon  35270  fineqvinfep  35306  subfacp1lem6  35413  wzel  36050  df3nandALT1  36627  df3nandALT2  36628  limsucncmpi  36673  weiunfr  36695  regsfromregtco  36766  unblimceq0  36813  bj-axseprep  37427  relowlpssretop  37726  pibt2  37779  nninfnub  38118  atlatmstc  39811  fnwe2lem2  43496  dfxor4  44210  pm10.57  44815  limclner  46094  limsupub  46147  limsuppnflem  46153  limsupre2lem  46167  icccncfext  46330  stoweidlem14  46457  stoweidlem34  46477  stoweidlem44  46487  ldepslinc  49000  fdomne0  49340  map0cor  49345  elsetrecslem  50189  alimp-no-surprise  50271