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  1494  nic-ax  1673  nic-axALT  1674  imnang  1842  dfsb3  2498  ralinexa  3090  pssn2lp  4079  indifdi  4269  disj  4425  disjsn  4687  sotric  5591  poirr2  6113  ordtri1  6385  funun  6582  imadif  6620  brprcneu  6866  brprcneuALT  6867  soisoi  7321  ordsucss  7812  ordunisuc2  7839  poseq  8157  oalimcl  8572  omlimcl  8590  unblem1  9300  suppr  9484  infpr  9517  cantnfp1lem3  9694  alephnbtwn  10085  kmlem4  10168  cfsuc  10271  isf32lem5  10371  hargch  10687  xrltnsym2  13154  fzp1nel  13628  fsumsplit  15757  sumsplit  15784  phiprmpw  16795  odzdvds  16815  pcdvdsb  16889  prmreclem5  16940  ramlb  17039  pltn2lp  18351  gsumzsplit  19908  dprdcntz2  20021  lbsextlem4  21122  obselocv  21688  psdmul  22104  maducoeval2  22578  lmmo  23318  kqcldsat  23671  rnelfmlem  23890  tsmssplit  24090  itg2splitlem  25701  itg2split  25702  fsumharmonic  26974  lgsne0  27298  lgsquadlem3  27345  2sqcoprm  27398  nosepssdm  27650  nosupbnd1lem4  27675  noinfbnd1lem4  27690  nocvxminlem  27741  axtgupdim2  28450  nmounbi  30757  hatomistici  32343  eliccelico  32754  elicoelioo  32755  nn0difffzod  32783  nn0min  32799  isarchi2  33183  archiabl  33196  oddpwdc  34386  eulerpartlemsv2  34390  eulerpartlems  34392  eulerpartlemv  34396  eulerpartlemgh  34410  eulerpartlemgs2  34412  ballotlemfrcn0  34562  bnj1533  34883  bnj1204  35043  bnj1280  35051  subfacp1lem6  35207  wzel  35842  df3nandALT1  36417  df3nandALT2  36418  limsucncmpi  36463  weiunfr  36485  unblimceq0  36525  relowlpssretop  37382  pibt2  37435  nninfnub  37775  atlatmstc  39337  fnwe2lem2  43075  dfxor4  43790  pm10.57  44395  limclner  45680  limsupub  45733  limsuppnflem  45739  limsupre2lem  45753  icccncfext  45916  stoweidlem14  46043  stoweidlem34  46063  stoweidlem44  46073  ldepslinc  48485  fdomne0  48828  map0cor  48833  elsetrecslem  49563  alimp-no-surprise  49645