Theorem imnan 391

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   ∧ wa 387

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 199  df-an 388

This theorem is referenced by:  imnani  392  iman  393  mpnanrd  401  nan  817  ianor  964  pm5.17  994  pm5.16  996  dn1  1038  nanimn  1466  nannanOLD  1471  nic-ax  1636  nic-axALT  1637  imnang  1804  dfsb3  2454  dfsb3ALT  2519  ralinexa  3210  pssn2lp  3968  disj  4282  disjsn  4521  sotric  5353  poirr2  5824  ordtri1  6062  funun  6233  imadif  6271  brprcneu  6491  soisoi  6904  ordsucss  7349  ordunisuc2  7375  oalimcl  7987  omlimcl  8005  unblem1  8565  suppr  8730  infpr  8762  cantnfp1lem3  8937  alephnbtwn  9291  kmlem4  9373  cfsuc  9477  isf32lem5  9577  hargch  9893  xrltnsym2  12348  fzp1nel  12807  fsumsplit  14957  sumsplit  14983  phiprmpw  15969  odzdvds  15988  pcdvdsb  16061  prmreclem5  16112  ramlb  16211  pltn2lp  17437  gsumzsplit  18800  dprdcntz2  18910  lbsextlem4  19655  obselocv  20574  maducoeval2  20953  lmmo  21692  kqcldsat  22045  rnelfmlem  22264  tsmssplit  22463  itg2splitlem  24052  itg2split  24053  fsumharmonic  25291  lgsne0  25613  lgsquadlem3  25660  2sqcoprm  25713  axtgupdim2  25959  nmounbi  28330  hatomistici  29920  eliccelico  30259  elicoelioo  30260  nn0min  30290  isarchi2  30486  archiabl  30499  oddpwdc  31263  eulerpartlemsv2  31267  eulerpartlems  31269  eulerpartlemv  31273  eulerpartlemgh  31287  eulerpartlemgs2  31289  ballotlemfrcn0  31439  bnj1533  31777  bnj1204  31935  bnj1280  31943  subfacp1lem6  32023  poseq  32622  wzel  32638  nosepssdm  32717  nosupbnd1lem4  32738  nocvxminlem  32774  df3nandALT1  33274  df3nandALT2  33275  limsucncmpi  33319  unblimceq0  33372  relowlpssretop  34093  pibt2  34145  nninfnub  34474  atlatmstc  35906  sn-dtru  38562  fnwe2lem2  39053  dfxor4  39480  pm10.57  40125  limclner  41369  limsupub  41422  limsuppnflem  41428  limsupre2lem  41442  icccncfext  41606  stoweidlem14  41736  stoweidlem34  41756  stoweidlem44  41766  ldepslinc  43937  elsetrecslem  44174  alimp-no-surprise  44255