Theorem imnan 403

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  imnani  404  iman  405  mpnanrd  413  nan  830  ianor  982  pm5.17  1012  pm5.16  1014  dn1  1058  dfnan2  1490  nic-ax  1681  nic-axALT  1682  imnang  1849  dfsb3  2497  ralinexa  3173  pssn2lp  4002  indifdi  4184  disj  4348  disjOLD  4349  disjsn  4613  sotric  5481  poirr2  5969  ordtri1  6224  funun  6404  imadif  6442  brprcneu  6686  fvprc  6687  soisoi  7115  ordsucss  7575  ordunisuc2  7601  oalimcl  8266  omlimcl  8284  unblem1  8901  suppr  9065  infpr  9097  cantnfp1lem3  9273  alephnbtwn  9650  kmlem4  9732  cfsuc  9836  isf32lem5  9936  hargch  10252  xrltnsym2  12693  fzp1nel  13161  fsumsplit  15269  sumsplit  15295  phiprmpw  16292  odzdvds  16311  pcdvdsb  16385  prmreclem5  16436  ramlb  16535  pltn2lp  17801  gsumzsplit  19266  dprdcntz2  19379  lbsextlem4  20152  obselocv  20644  maducoeval2  21491  lmmo  22231  kqcldsat  22584  rnelfmlem  22803  tsmssplit  23003  itg2splitlem  24600  itg2split  24601  fsumharmonic  25848  lgsne0  26170  lgsquadlem3  26217  2sqcoprm  26270  axtgupdim2  26516  nmounbi  28811  hatomistici  30397  nelbOLD  30490  eliccelico  30772  elicoelioo  30773  nn0min  30808  isarchi2  31112  archiabl  31125  oddpwdc  31987  eulerpartlemsv2  31991  eulerpartlems  31993  eulerpartlemv  31997  eulerpartlemgh  32011  eulerpartlemgs2  32013  ballotlemfrcn0  32162  bnj1533  32499  bnj1204  32659  bnj1280  32667  subfacp1lem6  32814  poseq  33482  wzel  33498  nosepssdm  33575  nosupbnd1lem4  33600  noinfbnd1lem4  33615  nocvxminlem  33658  df3nandALT1  34274  df3nandALT2  34275  limsucncmpi  34320  unblimceq0  34373  relowlpssretop  35221  pibt2  35274  nninfnub  35595  atlatmstc  37019  sn-dtru  39851  fnwe2lem2  40520  dfxor4  40992  pm10.57  41603  limclner  42810  limsupub  42863  limsuppnflem  42869  limsupre2lem  42883  icccncfext  43046  stoweidlem14  43173  stoweidlem34  43193  stoweidlem44  43203  ldepslinc  45466  fdomne0  45793  map0cor  45798  elsetrecslem  46018  alimp-no-surprise  46099