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  830  ianor  983  pm5.17  1013  pm5.16  1015  dn1  1057  dfnan2  1490  nic-ax  1669  nic-axALT  1670  imnang  1838  dfsb3  2496  ralinexa  3098  pssn2lp  4113  indifdi  4299  disj  4455  disjsn  4715  sotric  5625  poirr2  6146  ordtri1  6418  funun  6613  imadif  6651  brprcneu  6896  brprcneuALT  6897  soisoi  7347  ordsucss  7837  ordunisuc2  7864  poseq  8181  oalimcl  8596  omlimcl  8614  unblem1  9325  suppr  9508  infpr  9540  cantnfp1lem3  9717  alephnbtwn  10108  kmlem4  10191  cfsuc  10294  isf32lem5  10394  hargch  10710  xrltnsym2  13176  fzp1nel  13647  fsumsplit  15773  sumsplit  15800  phiprmpw  16809  odzdvds  16828  pcdvdsb  16902  prmreclem5  16953  ramlb  17052  pltn2lp  18398  gsumzsplit  19959  dprdcntz2  20072  lbsextlem4  21180  obselocv  21765  psdmul  22187  maducoeval2  22661  lmmo  23403  kqcldsat  23756  rnelfmlem  23975  tsmssplit  24175  itg2splitlem  25797  itg2split  25798  fsumharmonic  27069  lgsne0  27393  lgsquadlem3  27440  2sqcoprm  27493  nosepssdm  27745  nosupbnd1lem4  27770  noinfbnd1lem4  27785  nocvxminlem  27836  axtgupdim2  28493  nmounbi  30804  hatomistici  32390  eliccelico  32785  elicoelioo  32786  nn0difffzod  32813  nn0min  32826  isarchi2  33174  archiabl  33187  oddpwdc  34335  eulerpartlemsv2  34339  eulerpartlems  34341  eulerpartlemv  34345  eulerpartlemgh  34359  eulerpartlemgs2  34361  ballotlemfrcn0  34510  bnj1533  34844  bnj1204  35004  bnj1280  35012  subfacp1lem6  35169  wzel  35805  df3nandALT1  36381  df3nandALT2  36382  limsucncmpi  36427  weiunfr  36449  unblimceq0  36489  relowlpssretop  37346  pibt2  37399  nninfnub  37737  atlatmstc  39300  fnwe2lem2  43039  dfxor4  43755  pm10.57  44366  limclner  45606  limsupub  45659  limsuppnflem  45665  limsupre2lem  45679  icccncfext  45842  stoweidlem14  45969  stoweidlem34  45989  stoweidlem44  45999  ldepslinc  48354  fdomne0  48679  map0cor  48684  elsetrecslem  48929  alimp-no-surprise  49011