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  2492  ralinexa  3083  pssn2lp  4063  indifdi  4253  disj  4409  disjsn  4671  sotric  5569  poirr2  6085  ordtri1  6353  funun  6546  imadif  6584  brprcneu  6830  brprcneuALT  6831  soisoi  7285  ordsucss  7773  ordunisuc2  7800  poseq  8114  oalimcl  8501  omlimcl  8519  unblem1  9215  suppr  9399  infpr  9432  cantnfp1lem3  9609  alephnbtwn  10000  kmlem4  10083  cfsuc  10186  isf32lem5  10286  hargch  10602  xrltnsym2  13074  fzp1nel  13548  fsumsplit  15683  sumsplit  15710  phiprmpw  16722  odzdvds  16742  pcdvdsb  16816  prmreclem5  16867  ramlb  16966  pltn2lp  18280  gsumzsplit  19841  dprdcntz2  19954  lbsextlem4  21103  obselocv  21670  psdmul  22086  maducoeval2  22560  lmmo  23300  kqcldsat  23653  rnelfmlem  23872  tsmssplit  24072  itg2splitlem  25682  itg2split  25683  fsumharmonic  26955  lgsne0  27279  lgsquadlem3  27326  2sqcoprm  27379  nosepssdm  27631  nosupbnd1lem4  27656  noinfbnd1lem4  27671  nocvxminlem  27723  axtgupdim2  28451  nmounbi  30755  hatomistici  32341  eliccelico  32750  elicoelioo  32751  nn0difffzod  32779  nn0min  32795  isarchi2  33154  archiabl  33167  oddpwdc  34338  eulerpartlemsv2  34342  eulerpartlems  34344  eulerpartlemv  34348  eulerpartlemgh  34362  eulerpartlemgs2  34364  ballotlemfrcn0  34514  bnj1533  34835  bnj1204  34995  bnj1280  35003  subfacp1lem6  35165  wzel  35805  df3nandALT1  36380  df3nandALT2  36381  limsucncmpi  36426  weiunfr  36448  unblimceq0  36488  relowlpssretop  37345  pibt2  37398  nninfnub  37738  atlatmstc  39305  fnwe2lem2  43033  dfxor4  43748  pm10.57  44353  limclner  45642  limsupub  45695  limsuppnflem  45701  limsupre2lem  45715  icccncfext  45878  stoweidlem14  46005  stoweidlem34  46025  stoweidlem44  46035  ldepslinc  48491  fdomne0  48831  map0cor  48836  elsetrecslem  49681  alimp-no-surprise  49763