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

This theorem is referenced by:  imnani  400  iman  401  mpnanrd  409  nan  829  ianor  983  pm5.17  1013  pm5.16  1015  dn1  1057  dfnan2  1495  nic-ax  1674  nic-axALT  1675  imnang  1843  dfsb3  2494  ralinexa  3085  pssn2lp  4051  indifdi  4241  disj  4397  disjsn  4661  sotric  5552  poirr2  6070  ordtri1  6339  funun  6527  imadif  6565  brprcneu  6812  brprcneuALT  6813  soisoi  7262  ordsucss  7748  ordunisuc2  7774  poseq  8088  oalimcl  8475  omlimcl  8493  unblem1  9176  suppr  9356  infpr  9389  nelaneq  9487  cantnfp1lem3  9570  alephnbtwn  9962  kmlem4  10045  cfsuc  10148  isf32lem5  10248  hargch  10564  xrltnsym2  13037  fzp1nel  13511  fsumsplit  15648  sumsplit  15675  phiprmpw  16687  odzdvds  16707  pcdvdsb  16781  prmreclem5  16832  ramlb  16931  pltn2lp  18245  gsumzsplit  19839  dprdcntz2  19952  lbsextlem4  21098  obselocv  21665  psdmul  22081  maducoeval2  22555  lmmo  23295  kqcldsat  23648  rnelfmlem  23867  tsmssplit  24067  itg2splitlem  25676  itg2split  25677  fsumharmonic  26949  lgsne0  27273  lgsquadlem3  27320  2sqcoprm  27373  nosepssdm  27625  nosupbnd1lem4  27650  noinfbnd1lem4  27665  nocvxminlem  27717  axtgupdim2  28449  nmounbi  30756  hatomistici  32342  eliccelico  32760  elicoelioo  32761  nn0difffzod  32786  nn0min  32803  isarchi2  33154  archiabl  33167  extdgfialglem1  33705  oddpwdc  34367  eulerpartlemsv2  34371  eulerpartlems  34373  eulerpartlemv  34377  eulerpartlemgh  34391  eulerpartlemgs2  34393  ballotlemfrcn0  34543  bnj1533  34864  bnj1204  35024  bnj1280  35032  subfacp1lem6  35229  wzel  35866  df3nandALT1  36443  df3nandALT2  36444  limsucncmpi  36489  weiunfr  36511  unblimceq0  36551  relowlpssretop  37408  pibt2  37461  nninfnub  37801  atlatmstc  39428  fnwe2lem2  43154  dfxor4  43869  pm10.57  44474  limclner  45759  limsupub  45812  limsuppnflem  45818  limsupre2lem  45832  icccncfext  45995  stoweidlem14  46122  stoweidlem34  46142  stoweidlem44  46152  ldepslinc  48620  fdomne0  48960  map0cor  48965  elsetrecslem  49810  alimp-no-surprise  49892