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  830  ianor  984  pm5.17  1014  pm5.16  1016  dn1  1058  dfnan2  1496  nic-ax  1675  nic-axALT  1676  imnang  1844  dfsb3  2499  ralinexa  3091  pssn2lp  4058  indifdi  4248  disj  4404  disjsn  4670  sotric  5570  poirr2  6089  ordtri1  6358  funun  6546  imadif  6584  brprcneu  6832  brprcneuALT  6833  soisoi  7284  ordsucss  7770  ordunisuc2  7796  poseq  8110  oalimcl  8497  omlimcl  8515  unblem1  9204  suppr  9387  infpr  9420  nelaneq  9518  cantnfp1lem3  9601  alephnbtwn  9993  kmlem4  10076  cfsuc  10179  isf32lem5  10279  hargch  10596  xrltnsym2  13064  fzp1nel  13539  fsumsplit  15676  sumsplit  15703  phiprmpw  16715  odzdvds  16735  pcdvdsb  16809  prmreclem5  16860  ramlb  16959  pltn2lp  18274  gsumzsplit  19871  dprdcntz2  19984  lbsextlem4  21131  obselocv  21698  psdmul  22124  maducoeval2  22599  lmmo  23339  kqcldsat  23692  rnelfmlem  23911  tsmssplit  24111  itg2splitlem  25720  itg2split  25721  fsumharmonic  26993  lgsne0  27317  lgsquadlem3  27364  2sqcoprm  27417  nosepssdm  27669  nosupbnd1lem4  27694  noinfbnd1lem4  27709  nocvxminlem  27765  bdayfinbndlem1  28478  axtgupdim2  28559  nmounbi  30868  hatomistici  32454  eliccelico  32872  elicoelioo  32873  nn0difffzod  32899  nn0min  32916  isarchi2  33283  archiabl  33296  extdgfialglem1  33874  oddpwdc  34536  eulerpartlemsv2  34540  eulerpartlems  34542  eulerpartlemv  34546  eulerpartlemgh  34560  eulerpartlemgs2  34562  ballotlemfrcn0  34712  bnj1533  35032  bnj1204  35192  bnj1280  35200  xoromon  35270  fineqvinfep  35307  subfacp1lem6  35405  wzel  36042  df3nandALT1  36619  df3nandALT2  36620  limsucncmpi  36665  weiunfr  36687  regsfromregtr  36694  unblimceq0  36733  bj-axseprep  37326  relowlpssretop  37623  pibt2  37676  nninfnub  38006  atlatmstc  39699  fnwe2lem2  43412  dfxor4  44126  pm10.57  44731  limclner  46013  limsupub  46066  limsuppnflem  46072  limsupre2lem  46086  icccncfext  46249  stoweidlem14  46376  stoweidlem34  46396  stoweidlem44  46406  ldepslinc  48873  fdomne0  49213  map0cor  49218  elsetrecslem  50062  alimp-no-surprise  50144