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  2496  ralinexa  3086  pssn2lp  4053  indifdi  4243  disj  4399  disjsn  4663  sotric  5557  poirr2  6075  ordtri1  6344  funun  6532  imadif  6570  brprcneu  6818  brprcneuALT  6819  soisoi  7268  ordsucss  7754  ordunisuc2  7780  poseq  8094  oalimcl  8481  omlimcl  8499  unblem1  9183  suppr  9363  infpr  9396  nelaneq  9494  cantnfp1lem3  9577  alephnbtwn  9969  kmlem4  10052  cfsuc  10155  isf32lem5  10255  hargch  10571  xrltnsym2  13039  fzp1nel  13513  fsumsplit  15650  sumsplit  15677  phiprmpw  16689  odzdvds  16709  pcdvdsb  16783  prmreclem5  16834  ramlb  16933  pltn2lp  18247  gsumzsplit  19841  dprdcntz2  19954  lbsextlem4  21100  obselocv  21667  psdmul  22082  maducoeval2  22556  lmmo  23296  kqcldsat  23649  rnelfmlem  23868  tsmssplit  24068  itg2splitlem  25677  itg2split  25678  fsumharmonic  26950  lgsne0  27274  lgsquadlem3  27321  2sqcoprm  27374  nosepssdm  27626  nosupbnd1lem4  27651  noinfbnd1lem4  27666  nocvxminlem  27718  axtgupdim2  28450  nmounbi  30758  hatomistici  32344  eliccelico  32764  elicoelioo  32765  nn0difffzod  32791  nn0min  32808  isarchi2  33161  archiabl  33174  extdgfialglem1  33726  oddpwdc  34388  eulerpartlemsv2  34392  eulerpartlems  34394  eulerpartlemv  34398  eulerpartlemgh  34412  eulerpartlemgs2  34414  ballotlemfrcn0  34564  bnj1533  34885  bnj1204  35045  bnj1280  35053  subfacp1lem6  35250  wzel  35887  df3nandALT1  36464  df3nandALT2  36465  limsucncmpi  36510  weiunfr  36532  unblimceq0  36572  relowlpssretop  37429  pibt2  37482  nninfnub  37811  atlatmstc  39438  fnwe2lem2  43168  dfxor4  43883  pm10.57  44488  limclner  45773  limsupub  45826  limsuppnflem  45832  limsupre2lem  45846  icccncfext  46009  stoweidlem14  46136  stoweidlem34  46156  stoweidlem44  46166  ldepslinc  48634  fdomne0  48974  map0cor  48979  elsetrecslem  49824  alimp-no-surprise  49906