Theorem imnan 404

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

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

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 401

This theorem is used by:  imnani  405  iman  406  mpnanrd  414  nan  842  ianor  997  pm5.17  1029  pm5.16  1031  dn1  1073  dfnan2  1524  nic-ax  1703  nic-axALT  1704  imnang  1872  dfsb3  2526  ralinexa  3118  pssn2lp  4059  indifdi  4247  disj  4410  disjsn  4677  sotric  5599  poirr2  6124  ordtri1  6394  funun  6582  imadif  6620  brprcneu  6871  brprcneuALT  6872  soisoi  7326  ordsucss  7810  ordunisuc2  7836  poseq  8150  oalimcl  8541  omlimcl  8559  unblem1  9248  suppr  9428  infpr  9461  nelaneqOLD  9561  cantnfp1lem3  9645  alephnbtwn  10060  kmlem4  10142  cfsuc  10245  isf32lem5  10345  hargch  10662  xrltnsym2  13167  fzp1nel  13644  fsumsplit  15797  sumsplit  15824  phiprmpw  16839  odzdvds  16859  pcdvdsb  16933  prmreclem5  16984  ramlb  17083  pltn2lp  18399  gsumzsplit  20001  dprdcntz2  20114  lbsextlem4  21294  obselocv  21887  psdmul  22338  maducoeval2  22806  lmmo  23546  kqcldsat  23899  rnelfmlem  24118  tsmssplit  24318  itg2splitlem  25916  itg2split  25917  fsumharmonic  27185  lgsne0  27508  lgsquadlem3  27555  2sqcoprm  27608  nosepssdm  27859  nosupbnd1lem4  27884  noinfbnd1lem4  27899  nocvxminlem  27956  bdayfinbndlem1  28669  axtgupdim2  28749  nmounbi  31137  hatomistici  32723  eliccelico  33131  elicoelioo  33132  nn0difffzod  33158  nn0min  33174  isarchi2  33514  archiabl  33527  extdgfialglem1  34091  oddpwdc  34753  eulerpartlemsv2  34757  eulerpartlems  34759  eulerpartlemv  34763  eulerpartlemgh  34777  eulerpartlemgs2  34779  ballotlemfrcn0  34929  bnj1533  35249  bnj1204  35409  bnj1280  35417  xoromon  35488  fineqvinfep  35546  subfacp1lem6  35685  wzel  36322  df3nandALT1  36938  df3nandALT2  36939  limsucncmpi  36984  weiunfr  37006  regsfromregtco  37077  unblimceq0  37124  bj-axseprep  37739  relowlpssretop  38038  pibt2  38091  nninfnub  38430  atlatmstc  40121  fnwe2lem2  43806  dfxor4  44520  pm10.57  45109  limclner  46393  limsupub  46446  limsuppnflem  46452  limsupre2lem  46466  icccncfext  46629  stoweidlem14  46756  stoweidlem34  46776  stoweidlem44  46786  ldepslinc  49317  fdomne0  49656  map0cor  49661  elsetrecslem  50505  alimp-no-surprise  50587