Theorem imnan 401

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  imnani  402  iman  403  mpnanrd  411  nan  828  ianor  980  pm5.17  1010  pm5.16  1012  dn1  1056  dfnan2  1492  nic-ax  1675  nic-axALT  1676  imnang  1844  dfsb3  2497  ralinexa  3102  pssn2lp  4056  indifdi  4238  disj  4402  disjOLD  4403  disjsn  4667  exexneq  5386  sotric  5567  poirr2  6071  ordtri1  6343  funun  6539  imadif  6577  brprcneu  6824  brprcneuALT  6825  soisoi  7264  ordsucss  7740  ordunisuc2  7767  poseq  8054  oalimcl  8471  omlimcl  8489  unblem1  9169  suppr  9337  infpr  9369  cantnfp1lem3  9546  alephnbtwn  9937  kmlem4  10019  cfsuc  10123  isf32lem5  10223  hargch  10539  xrltnsym2  12982  fzp1nel  13450  fsumsplit  15557  sumsplit  15584  phiprmpw  16579  odzdvds  16598  pcdvdsb  16672  prmreclem5  16723  ramlb  16822  pltn2lp  18161  gsumzsplit  19627  dprdcntz2  19740  lbsextlem4  20533  obselocv  21045  maducoeval2  21899  lmmo  22641  kqcldsat  22994  rnelfmlem  23213  tsmssplit  23413  itg2splitlem  25023  itg2split  25024  fsumharmonic  26271  lgsne0  26593  lgsquadlem3  26640  2sqcoprm  26693  nosepssdm  26944  nosupbnd1lem4  26969  noinfbnd1lem4  26984  nocvxminlem  27027  axtgupdim2  27187  nmounbi  29492  hatomistici  31078  eliccelico  31449  elicoelioo  31450  nn0min  31485  isarchi2  31790  archiabl  31803  oddpwdc  32685  eulerpartlemsv2  32689  eulerpartlems  32691  eulerpartlemv  32695  eulerpartlemgh  32709  eulerpartlemgs2  32711  ballotlemfrcn0  32860  bnj1533  33195  bnj1204  33355  bnj1280  33363  subfacp1lem6  33510  wzel  34161  df3nandALT1  34727  df3nandALT2  34728  limsucncmpi  34773  unblimceq0  34826  relowlpssretop  35691  pibt2  35744  nninfnub  36065  atlatmstc  37637  fnwe2lem2  41190  dfxor4  41747  pm10.57  42362  limclner  43580  limsupub  43633  limsuppnflem  43639  limsupre2lem  43653  icccncfext  43816  stoweidlem14  43943  stoweidlem34  43963  stoweidlem44  43973  ldepslinc  46268  fdomne0  46594  map0cor  46599  elsetrecslem  46821  alimp-no-surprise  46902