Theorem imnan 405

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  imnani  406  iman  407  mpnanrd  415  nan  843  ianor  997  pm5.17  1029  pm5.16  1031  dn1  1073  dfnan2  1523  nic-ax  1705  nic-axALT  1706  imnang  1874  dfsb3  2526  ralinexa  3118  pssn2lp  4034  indifdi  4241  disj  4405  disjsn  4671  sotric  5592  poirr2  6123  ordtri1  6402  funun  6594  imadif  6632  brprcneu  6883  brprcneuALT  6884  soisoi  7343  ordsucss  7836  ordunisuc2  7862  fnwe2lem3  8157  poseq  8185  oalimcl  8579  omlimcl  8597  unblem1  9295  suppr  9474  infpr  9507  nelaneqOLD  9607  cantnfp1lem3  9691  alephnbtwn  10160  kmlem4  10242  cfsuc  10345  isf32lem5  10445  hargch  10768  xrltnsym2  13277  fzp1nel  13755  fsumsplit  15919  sumsplit  15946  phiprmpw  16965  odzdvds  16985  pcdvdsb  17059  prmreclem5  17110  ramlb  17209  pltn2lp  18525  gsumzsplit  20153  dprdcntz2  20266  lbsextlem4  21451  obselocv  22046  psdmul  22499  maducoeval2  22967  lmmo  23710  kqcldsat  24064  rnelfmlem  24283  tsmssplit  24483  itg2splitlem  26081  itg2split  26082  fsumharmonic  27351  lgsne0  27674  lgsquadlem3  27721  2sqcoprm  27774  nosepssdm  28055  nosupbnd1lem4  28080  noinfbnd1lem4  28095  nocvxminlem  28152  bdayfinbndlem1  28865  axtgupdim2  28945  nmounbi  31390  hatomistici  32976  eliccelico  33422  elicoelioo  33423  nn0difffzod  33449  nn0min  33465  isarchi2  33799  archiabl  33812  extdgfialglem1  34377  oddpwdc  35039  eulerpartlemsv2  35043  eulerpartlems  35045  eulerpartlemv  35049  eulerpartlemgh  35063  eulerpartlemgs2  35065  ballotlemfrcn0  35215  bnj1533  35535  bnj1204  35695  bnj1280  35703  xoromon  35774  fineqvinfep  35864  subfacp1lem6  36071  wzel  36713  df3nandALT1  37314  df3nandALT2  37315  limsucncmpi  37360  weiunfr  37382  regsfromregtco  37453  unblimceq0  37500  bj-axseprep  38129  relowlpssretop  38427  pibt2  38480  nninfnub  38825  atlatmstc  40516  dfxor4  44906  pm10.57  45495  limclner  46800  limsupub  46853  limsuppnflem  46859  limsupre2lem  46873  icccncfext  47036  stoweidlem14  47163  stoweidlem34  47183  stoweidlem44  47193  ldepslinc  49760  fdomne0  50100  map0cor  50105  elsetrecslem  51006  alimp-no-surprise  51091