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  3087  pssn2lp  4054  indifdi  4244  disj  4400  disjsn  4666  sotric  5560  poirr2  6079  ordtri1  6348  funun  6536  imadif  6574  brprcneu  6822  brprcneuALT  6823  soisoi  7272  ordsucss  7758  ordunisuc2  7784  poseq  8098  oalimcl  8485  omlimcl  8503  unblem1  9190  suppr  9373  infpr  9406  nelaneq  9504  cantnfp1lem3  9587  alephnbtwn  9979  kmlem4  10062  cfsuc  10165  isf32lem5  10265  hargch  10582  xrltnsym2  13050  fzp1nel  13525  fsumsplit  15662  sumsplit  15689  phiprmpw  16701  odzdvds  16721  pcdvdsb  16795  prmreclem5  16846  ramlb  16945  pltn2lp  18260  gsumzsplit  19854  dprdcntz2  19967  lbsextlem4  21114  obselocv  21681  psdmul  22107  maducoeval2  22582  lmmo  23322  kqcldsat  23675  rnelfmlem  23894  tsmssplit  24094  itg2splitlem  25703  itg2split  25704  fsumharmonic  26976  lgsne0  27300  lgsquadlem3  27347  2sqcoprm  27400  nosepssdm  27652  nosupbnd1lem4  27677  noinfbnd1lem4  27692  nocvxminlem  27744  axtgupdim2  28492  nmounbi  30800  hatomistici  32386  eliccelico  32806  elicoelioo  32807  nn0difffzod  32833  nn0min  32850  isarchi2  33216  archiabl  33229  extdgfialglem1  33798  oddpwdc  34460  eulerpartlemsv2  34464  eulerpartlems  34466  eulerpartlemv  34470  eulerpartlemgh  34484  eulerpartlemgs2  34486  ballotlemfrcn0  34636  bnj1533  34957  bnj1204  35117  bnj1280  35125  xoromon  35194  fineqvinfep  35230  subfacp1lem6  35328  wzel  35965  df3nandALT1  36542  df3nandALT2  36543  limsucncmpi  36588  weiunfr  36610  unblimceq0  36650  relowlpssretop  37508  pibt2  37561  nninfnub  37891  atlatmstc  39518  fnwe2lem2  43235  dfxor4  43949  pm10.57  44554  limclner  45837  limsupub  45890  limsuppnflem  45896  limsupre2lem  45910  icccncfext  46073  stoweidlem14  46200  stoweidlem34  46220  stoweidlem44  46230  ldepslinc  48697  fdomne0  49037  map0cor  49042  elsetrecslem  49886  alimp-no-surprise  49968