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  1524  nic-ax  1706  nic-axALT  1707  imnang  1875  dfsb3  2524  ralinexa  3116  pssn2lp  4053  indifdi  4240  disj  4403  disjsn  4672  sotric  5589  poirr2  6118  ordtri1  6396  funun  6586  imadif  6624  brprcneu  6875  brprcneuALT  6876  soisoi  7336  ordsucss  7829  ordunisuc2  7855  fnwe2lem3  8147  poseq  8175  oalimcl  8568  omlimcl  8586  unblem1  9284  suppr  9464  infpr  9497  nelaneqOLD  9597  cantnfp1lem3  9681  alephnbtwn  10150  kmlem4  10232  cfsuc  10335  isf32lem5  10435  hargch  10758  xrltnsym2  13267  fzp1nel  13745  fsumsplit  15907  sumsplit  15934  phiprmpw  16953  odzdvds  16973  pcdvdsb  17047  prmreclem5  17098  ramlb  17197  pltn2lp  18513  gsumzsplit  20141  dprdcntz2  20254  lbsextlem4  21439  obselocv  22034  psdmul  22487  maducoeval2  22955  lmmo  23698  kqcldsat  24052  rnelfmlem  24271  tsmssplit  24471  itg2splitlem  26069  itg2split  26070  fsumharmonic  27339  lgsne0  27662  lgsquadlem3  27709  2sqcoprm  27762  nosepssdm  28043  nosupbnd1lem4  28068  noinfbnd1lem4  28083  nocvxminlem  28140  bdayfinbndlem1  28853  axtgupdim2  28933  nmounbi  31378  hatomistici  32964  eliccelico  33369  elicoelioo  33370  nn0difffzod  33396  nn0min  33412  isarchi2  33746  archiabl  33759  extdgfialglem1  34324  oddpwdc  34986  eulerpartlemsv2  34990  eulerpartlems  34992  eulerpartlemv  34996  eulerpartlemgh  35010  eulerpartlemgs2  35012  ballotlemfrcn0  35162  bnj1533  35482  bnj1204  35642  bnj1280  35650  xoromon  35716  fineqvinfep  35793  subfacp1lem6  35950  wzel  36586  df3nandALT1  37187  df3nandALT2  37188  limsucncmpi  37233  weiunfr  37255  regsfromregtco  37326  unblimceq0  37373  bj-axseprep  37990  relowlpssretop  38287  pibt2  38340  nninfnub  38685  atlatmstc  40376  dfxor4  44765  pm10.57  45354  limclner  46660  limsupub  46713  limsuppnflem  46719  limsupre2lem  46733  icccncfext  46896  stoweidlem14  47023  stoweidlem34  47043  stoweidlem44  47053  ldepslinc  49620  fdomne0  49959  map0cor  49964  elsetrecslem  50791  alimp-no-surprise  50876