Theorem imnan 403

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  imnani  404  iman  405  mpnanrd  413  nan  840  ianor  995  pm5.17  1025  pm5.16  1027  dn1  1069  dfnan2  1514  nic-ax  1693  nic-axALT  1694  imnang  1862  dfsb3  2525  ralinexa  3115  pssn2lp  4058  indifdi  4246  disj  4404  disjsn  4670  sotric  5585  poirr2  6111  ordtri1  6379  funun  6567  imadif  6605  brprcneu  6857  brprcneuALT  6858  soisoi  7312  ordsucss  7798  ordunisuc2  7824  poseq  8138  oalimcl  8529  omlimcl  8547  unblem1  9236  suppr  9418  infpr  9451  nelaneqOLD  9551  cantnfp1lem3  9635  alephnbtwn  10027  kmlem4  10110  cfsuc  10214  isf32lem5  10314  hargch  10631  xrltnsym2  13140  fzp1nel  13616  fsumsplit  15768  sumsplit  15795  phiprmpw  16811  odzdvds  16831  pcdvdsb  16905  prmreclem5  16956  ramlb  17055  pltn2lp  18371  gsumzsplit  19967  dprdcntz2  20080  lbsextlem4  21231  obselocv  21780  psdmul  22231  maducoeval2  22700  lmmo  23440  kqcldsat  23793  rnelfmlem  24012  tsmssplit  24212  itg2splitlem  25810  itg2split  25811  fsumharmonic  27076  lgsne0  27399  lgsquadlem3  27446  2sqcoprm  27499  nosepssdm  27750  nosupbnd1lem4  27775  noinfbnd1lem4  27790  nocvxminlem  27847  bdayfinbndlem1  28560  axtgupdim2  28640  nmounbi  30979  hatomistici  32565  eliccelico  32979  elicoelioo  32980  nn0difffzod  33006  nn0min  33023  isarchi2  33365  archiabl  33378  extdgfialglem1  33989  oddpwdc  34651  eulerpartlemsv2  34655  eulerpartlems  34657  eulerpartlemv  34661  eulerpartlemgh  34675  eulerpartlemgs2  34677  ballotlemfrcn0  34827  bnj1533  35147  bnj1204  35307  bnj1280  35315  xoromon  35384  fineqvinfep  35421  subfacp1lem6  35535  wzel  36172  df3nandALT1  36759  df3nandALT2  36760  limsucncmpi  36805  weiunfr  36827  regsfromregtco  36898  unblimceq0  36945  bj-axseprep  37559  relowlpssretop  37858  pibt2  37911  nninfnub  38250  atlatmstc  39943  fnwe2lem2  43628  dfxor4  44342  pm10.57  44947  limclner  46225  limsupub  46278  limsuppnflem  46284  limsupre2lem  46298  icccncfext  46461  stoweidlem14  46588  stoweidlem34  46608  stoweidlem44  46618  ldepslinc  49131  fdomne0  49471  map0cor  49476  elsetrecslem  50320  alimp-no-surprise  50402