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  829  ianor  983  pm5.17  1013  pm5.16  1015  dn1  1057  dfnan2  1494  nic-ax  1673  nic-axALT  1674  imnang  1842  dfsb3  2492  ralinexa  3083  pssn2lp  4067  indifdi  4257  disj  4413  disjsn  4675  sotric  5576  poirr2  6097  ordtri1  6365  funun  6562  imadif  6600  brprcneu  6848  brprcneuALT  6849  soisoi  7303  ordsucss  7793  ordunisuc2  7820  poseq  8137  oalimcl  8524  omlimcl  8542  unblem1  9239  suppr  9423  infpr  9456  cantnfp1lem3  9633  alephnbtwn  10024  kmlem4  10107  cfsuc  10210  isf32lem5  10310  hargch  10626  xrltnsym2  13098  fzp1nel  13572  fsumsplit  15707  sumsplit  15734  phiprmpw  16746  odzdvds  16766  pcdvdsb  16840  prmreclem5  16891  ramlb  16990  pltn2lp  18300  gsumzsplit  19857  dprdcntz2  19970  lbsextlem4  21071  obselocv  21637  psdmul  22053  maducoeval2  22527  lmmo  23267  kqcldsat  23620  rnelfmlem  23839  tsmssplit  24039  itg2splitlem  25649  itg2split  25650  fsumharmonic  26922  lgsne0  27246  lgsquadlem3  27293  2sqcoprm  27346  nosepssdm  27598  nosupbnd1lem4  27623  noinfbnd1lem4  27638  nocvxminlem  27689  axtgupdim2  28398  nmounbi  30705  hatomistici  32291  eliccelico  32700  elicoelioo  32701  nn0difffzod  32729  nn0min  32745  isarchi2  33139  archiabl  33152  oddpwdc  34345  eulerpartlemsv2  34349  eulerpartlems  34351  eulerpartlemv  34355  eulerpartlemgh  34369  eulerpartlemgs2  34371  ballotlemfrcn0  34521  bnj1533  34842  bnj1204  35002  bnj1280  35010  subfacp1lem6  35172  wzel  35812  df3nandALT1  36387  df3nandALT2  36388  limsucncmpi  36433  weiunfr  36455  unblimceq0  36495  relowlpssretop  37352  pibt2  37405  nninfnub  37745  atlatmstc  39312  fnwe2lem2  43040  dfxor4  43755  pm10.57  44360  limclner  45649  limsupub  45702  limsuppnflem  45708  limsupre2lem  45722  icccncfext  45885  stoweidlem14  46012  stoweidlem34  46032  stoweidlem44  46042  ldepslinc  48498  fdomne0  48838  map0cor  48843  elsetrecslem  49688  alimp-no-surprise  49770