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  2498  ralinexa  3090  pssn2lp  4044  indifdi  4234  disj  4390  disjsn  4655  sotric  5569  poirr2  6087  ordtri1  6356  funun  6544  imadif  6582  brprcneu  6830  brprcneuALT  6831  soisoi  7283  ordsucss  7769  ordunisuc2  7795  poseq  8108  oalimcl  8495  omlimcl  8513  unblem1  9202  suppr  9385  infpr  9418  nelaneqOLD  9517  cantnfp1lem3  9601  alephnbtwn  9993  kmlem4  10076  cfsuc  10179  isf32lem5  10279  hargch  10596  xrltnsym2  13089  fzp1nel  13565  fsumsplit  15703  sumsplit  15730  phiprmpw  16746  odzdvds  16766  pcdvdsb  16840  prmreclem5  16891  ramlb  16990  pltn2lp  18305  gsumzsplit  19902  dprdcntz2  20015  lbsextlem4  21159  obselocv  21708  psdmul  22132  maducoeval2  22605  lmmo  23345  kqcldsat  23698  rnelfmlem  23917  tsmssplit  24117  itg2splitlem  25715  itg2split  25716  fsumharmonic  26975  lgsne0  27298  lgsquadlem3  27345  2sqcoprm  27398  nosepssdm  27650  nosupbnd1lem4  27675  noinfbnd1lem4  27690  nocvxminlem  27746  bdayfinbndlem1  28459  axtgupdim2  28539  nmounbi  30847  hatomistici  32433  eliccelico  32850  elicoelioo  32851  nn0difffzod  32877  nn0min  32894  isarchi2  33246  archiabl  33259  extdgfialglem1  33836  oddpwdc  34498  eulerpartlemsv2  34502  eulerpartlems  34504  eulerpartlemv  34508  eulerpartlemgh  34522  eulerpartlemgs2  34524  ballotlemfrcn0  34674  bnj1533  34994  bnj1204  35154  bnj1280  35162  xoromon  35232  fineqvinfep  35269  subfacp1lem6  35367  wzel  36004  df3nandALT1  36581  df3nandALT2  36582  limsucncmpi  36627  weiunfr  36649  regsfromregtco  36720  unblimceq0  36767  bj-axseprep  37381  relowlpssretop  37680  pibt2  37733  nninfnub  38072  atlatmstc  39765  fnwe2lem2  43479  dfxor4  44193  pm10.57  44798  limclner  46079  limsupub  46132  limsuppnflem  46138  limsupre2lem  46152  icccncfext  46315  stoweidlem14  46442  stoweidlem34  46462  stoweidlem44  46472  ldepslinc  48985  fdomne0  49325  map0cor  49330  elsetrecslem  50174  alimp-no-surprise  50256