Theorem imnan 405

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  imnani  406  iman  407  mpnanrd  415  nan  843  ianor  997  pm5.17  1029  pm5.16  1031  dn1  1073  dfnan2  1524  nic-ax  1706  nic-axALT  1707  imnang  1875  dfsb3  2523  ralinexa  3115  pssn2lp  4053  indifdi  4240  disj  4403  disjsn  4672  sotric  5593  poirr2  6118  ordtri1  6391  funun  6580  imadif  6618  brprcneu  6869  brprcneuALT  6870  soisoi  7330  ordsucss  7815  ordunisuc2  7841  poseq  8157  oalimcl  8550  omlimcl  8568  unblem1  9265  suppr  9445  infpr  9478  nelaneqOLD  9578  cantnfp1lem3  9662  alephnbtwn  10077  kmlem4  10159  cfsuc  10262  isf32lem5  10362  hargch  10685  xrltnsym2  13192  fzp1nel  13669  fsumsplit  15830  sumsplit  15857  phiprmpw  16870  odzdvds  16890  pcdvdsb  16964  prmreclem5  17015  ramlb  17114  pltn2lp  18430  gsumzsplit  20057  dprdcntz2  20170  lbsextlem4  21351  obselocv  21944  psdmul  22397  maducoeval2  22865  lmmo  23608  kqcldsat  23962  rnelfmlem  24181  tsmssplit  24381  itg2splitlem  25979  itg2split  25980  fsumharmonic  27251  lgsne0  27574  lgsquadlem3  27621  2sqcoprm  27674  nosepssdm  27925  nosupbnd1lem4  27950  noinfbnd1lem4  27965  nocvxminlem  28022  bdayfinbndlem1  28735  axtgupdim2  28815  nmounbi  31260  hatomistici  32846  eliccelico  33251  elicoelioo  33252  nn0difffzod  33278  nn0min  33294  isarchi2  33628  archiabl  33641  extdgfialglem1  34205  oddpwdc  34868  eulerpartlemsv2  34872  eulerpartlems  34874  eulerpartlemv  34878  eulerpartlemgh  34892  eulerpartlemgs2  34894  ballotlemfrcn0  35044  bnj1533  35364  bnj1204  35524  bnj1280  35532  xoromon  35596  fineqvinfep  35654  subfacp1lem6  35767  wzel  36404  df3nandALT1  37021  df3nandALT2  37022  limsucncmpi  37067  weiunfr  37089  regsfromregtco  37160  unblimceq0  37207  bj-axseprep  37822  relowlpssretop  38121  pibt2  38174  nninfnub  38504  atlatmstc  40195  fnwe2lem2  43895  dfxor4  44609  pm10.57  45198  limclner  46482  limsupub  46535  limsuppnflem  46541  limsupre2lem  46555  icccncfext  46718  stoweidlem14  46845  stoweidlem34  46865  stoweidlem44  46875  ldepslinc  49442  fdomne0  49781  map0cor  49786  elsetrecslem  50628  alimp-no-surprise  50713