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  1029  pm5.16  1031  dn1  1073  dfnan2  1524  nic-ax  1703  nic-axALT  1704  imnang  1872  dfsb3  2526  ralinexa  3118  pssn2lp  4059  indifdi  4247  disj  4410  disjsn  4677  sotric  5599  poirr2  6124  ordtri1  6394  funun  6582  imadif  6620  brprcneu  6871  brprcneuALT  6872  soisoi  7326  ordsucss  7810  ordunisuc2  7836  poseq  8150  oalimcl  8541  omlimcl  8559  unblem1  9248  suppr  9428  infpr  9461  nelaneqOLD  9561  cantnfp1lem3  9645  alephnbtwn  10051  kmlem4  10133  cfsuc  10236  isf32lem5  10336  hargch  10653  xrltnsym2  13158  fzp1nel  13635  fsumsplit  15788  sumsplit  15815  phiprmpw  16830  odzdvds  16850  pcdvdsb  16924  prmreclem5  16975  ramlb  17074  pltn2lp  18390  gsumzsplit  19992  dprdcntz2  20105  lbsextlem4  21285  obselocv  21878  psdmul  22329  maducoeval2  22797  lmmo  23537  kqcldsat  23890  rnelfmlem  24109  tsmssplit  24309  itg2splitlem  25907  itg2split  25908  fsumharmonic  27176  lgsne0  27499  lgsquadlem3  27546  2sqcoprm  27599  nosepssdm  27850  nosupbnd1lem4  27875  noinfbnd1lem4  27890  nocvxminlem  27947  bdayfinbndlem1  28660  axtgupdim2  28740  nmounbi  31128  hatomistici  32714  eliccelico  33122  elicoelioo  33123  nn0difffzod  33149  nn0min  33165  isarchi2  33505  archiabl  33518  extdgfialglem1  34082  oddpwdc  34744  eulerpartlemsv2  34748  eulerpartlems  34750  eulerpartlemv  34754  eulerpartlemgh  34768  eulerpartlemgs2  34770  ballotlemfrcn0  34920  bnj1533  35240  bnj1204  35400  bnj1280  35408  xoromon  35479  fineqvinfep  35538  subfacp1lem6  35677  wzel  36314  df3nandALT1  36930  df3nandALT2  36931  limsucncmpi  36976  weiunfr  36998  regsfromregtco  37069  unblimceq0  37116  bj-axseprep  37731  relowlpssretop  38030  pibt2  38083  nninfnub  38422  atlatmstc  40113  fnwe2lem2  43798  dfxor4  44512  pm10.57  45101  limclner  46385  limsupub  46438  limsuppnflem  46444  limsupre2lem  46458  icccncfext  46621  stoweidlem14  46748  stoweidlem34  46768  stoweidlem44  46778  ldepslinc  49309  fdomne0  49648  map0cor  49653  elsetrecslem  50497  alimp-no-surprise  50579