Theorem imnan 402

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  imnani  403  iman  404  mpnanrd  412  nan  827  ianor  978  pm5.17  1008  pm5.16  1010  dn1  1052  nanimn  1484  nic-ax  1674  nic-axALT  1675  imnang  1842  dfsb3  2533  dfsb3ALT  2592  ralinexa  3266  pssn2lp  4080  disj  4401  disjsn  4649  sotric  5503  poirr2  5986  ordtri1  6226  funun  6402  imadif  6440  brprcneu  6664  soisoi  7083  ordsucss  7535  ordunisuc2  7561  oalimcl  8188  omlimcl  8206  unblem1  8772  suppr  8937  infpr  8969  cantnfp1lem3  9145  alephnbtwn  9499  kmlem4  9581  cfsuc  9681  isf32lem5  9781  hargch  10097  xrltnsym2  12534  fzp1nel  12994  fsumsplit  15099  sumsplit  15125  phiprmpw  16115  odzdvds  16134  pcdvdsb  16207  prmreclem5  16258  ramlb  16357  pltn2lp  17581  gsumzsplit  19049  dprdcntz2  19162  lbsextlem4  19935  obselocv  20874  maducoeval2  21251  lmmo  21990  kqcldsat  22343  rnelfmlem  22562  tsmssplit  22762  itg2splitlem  24351  itg2split  24352  fsumharmonic  25591  lgsne0  25913  lgsquadlem3  25960  2sqcoprm  26013  axtgupdim2  26259  nmounbi  28555  hatomistici  30141  nelbOLD  30234  eliccelico  30502  elicoelioo  30503  nn0min  30538  isarchi2  30816  archiabl  30829  oddpwdc  31614  eulerpartlemsv2  31618  eulerpartlems  31620  eulerpartlemv  31624  eulerpartlemgh  31638  eulerpartlemgs2  31640  ballotlemfrcn0  31789  bnj1533  32126  bnj1204  32286  bnj1280  32294  subfacp1lem6  32434  poseq  33097  wzel  33113  nosepssdm  33192  nosupbnd1lem4  33213  nocvxminlem  33249  df3nandALT1  33749  df3nandALT2  33750  limsucncmpi  33795  unblimceq0  33848  relowlpssretop  34647  pibt2  34700  nninfnub  35028  atlatmstc  36457  sn-dtru  39118  fnwe2lem2  39658  dfxor4  40118  pm10.57  40710  limclner  41939  limsupub  41992  limsuppnflem  41998  limsupre2lem  42012  icccncfext  42177  stoweidlem14  42306  stoweidlem34  42326  stoweidlem44  42336  ldepslinc  44571  elsetrecslem  44808  alimp-no-surprise  44889