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 205   ∧ 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 206  df-an 396

This theorem is referenced by:  imnani  400  iman  401  mpnanrd  409  nan  826  ianor  978  pm5.17  1008  pm5.16  1010  dn1  1054  dfnan2  1486  nic-ax  1677  nic-axALT  1678  imnang  1845  dfsb3  2498  ralinexa  3190  pssn2lp  4032  indifdi  4214  disj  4378  disjOLD  4379  disjsn  4644  sotric  5522  poirr2  6018  ordtri1  6284  funun  6464  imadif  6502  brprcneu  6747  fvprc  6748  soisoi  7179  ordsucss  7640  ordunisuc2  7666  oalimcl  8353  omlimcl  8371  unblem1  8996  suppr  9160  infpr  9192  cantnfp1lem3  9368  alephnbtwn  9758  kmlem4  9840  cfsuc  9944  isf32lem5  10044  hargch  10360  xrltnsym2  12801  fzp1nel  13269  fsumsplit  15381  sumsplit  15408  phiprmpw  16405  odzdvds  16424  pcdvdsb  16498  prmreclem5  16549  ramlb  16648  pltn2lp  17974  gsumzsplit  19443  dprdcntz2  19556  lbsextlem4  20338  obselocv  20845  maducoeval2  21697  lmmo  22439  kqcldsat  22792  rnelfmlem  23011  tsmssplit  23211  itg2splitlem  24818  itg2split  24819  fsumharmonic  26066  lgsne0  26388  lgsquadlem3  26435  2sqcoprm  26488  axtgupdim2  26736  nmounbi  29039  hatomistici  30625  nelbOLDOLD  30718  eliccelico  31000  elicoelioo  31001  nn0min  31036  isarchi2  31341  archiabl  31354  oddpwdc  32221  eulerpartlemsv2  32225  eulerpartlems  32227  eulerpartlemv  32231  eulerpartlemgh  32245  eulerpartlemgs2  32247  ballotlemfrcn0  32396  bnj1533  32732  bnj1204  32892  bnj1280  32900  subfacp1lem6  33047  poseq  33729  wzel  33745  nosepssdm  33816  nosupbnd1lem4  33841  noinfbnd1lem4  33856  nocvxminlem  33899  df3nandALT1  34515  df3nandALT2  34516  limsucncmpi  34561  unblimceq0  34614  relowlpssretop  35462  pibt2  35515  nninfnub  35836  atlatmstc  37260  sn-dtru  40116  fnwe2lem2  40792  dfxor4  41263  pm10.57  41878  limclner  43082  limsupub  43135  limsuppnflem  43141  limsupre2lem  43155  icccncfext  43318  stoweidlem14  43445  stoweidlem34  43465  stoweidlem44  43475  ldepslinc  45738  fdomne0  46065  map0cor  46070  elsetrecslem  46290  alimp-no-surprise  46371