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  982  pm5.17  1012  pm5.16  1014  dn1  1058  dfnan2  1491  nic-ax  1671  nic-axALT  1672  imnang  1840  dfsb3  2502  ralinexa  3107  pssn2lp  4127  indifdi  4313  disj  4473  disjsn  4736  sotric  5637  poirr2  6156  ordtri1  6428  funun  6624  imadif  6662  brprcneu  6910  brprcneuALT  6911  soisoi  7364  ordsucss  7854  ordunisuc2  7881  poseq  8199  oalimcl  8616  omlimcl  8634  unblem1  9356  suppr  9540  infpr  9572  cantnfp1lem3  9749  alephnbtwn  10140  kmlem4  10223  cfsuc  10326  isf32lem5  10426  hargch  10742  xrltnsym2  13200  fzp1nel  13668  fsumsplit  15789  sumsplit  15816  phiprmpw  16823  odzdvds  16842  pcdvdsb  16916  prmreclem5  16967  ramlb  17066  pltn2lp  18411  gsumzsplit  19969  dprdcntz2  20082  lbsextlem4  21186  obselocv  21771  psdmul  22193  maducoeval2  22667  lmmo  23409  kqcldsat  23762  rnelfmlem  23981  tsmssplit  24181  itg2splitlem  25803  itg2split  25804  fsumharmonic  27073  lgsne0  27397  lgsquadlem3  27444  2sqcoprm  27497  nosepssdm  27749  nosupbnd1lem4  27774  noinfbnd1lem4  27789  nocvxminlem  27840  axtgupdim2  28497  nmounbi  30808  hatomistici  32394  eliccelico  32782  elicoelioo  32783  nn0difffzod  32811  nn0min  32824  isarchi2  33165  archiabl  33178  oddpwdc  34319  eulerpartlemsv2  34323  eulerpartlems  34325  eulerpartlemv  34329  eulerpartlemgh  34343  eulerpartlemgs2  34345  ballotlemfrcn0  34494  bnj1533  34828  bnj1204  34988  bnj1280  34996  subfacp1lem6  35153  wzel  35788  df3nandALT1  36365  df3nandALT2  36366  limsucncmpi  36411  weiunfr  36433  unblimceq0  36473  relowlpssretop  37330  pibt2  37383  nninfnub  37711  atlatmstc  39275  fnwe2lem2  43008  dfxor4  43728  pm10.57  44340  limclner  45572  limsupub  45625  limsuppnflem  45631  limsupre2lem  45645  icccncfext  45808  stoweidlem14  45935  stoweidlem34  45955  stoweidlem44  45965  ldepslinc  48238  fdomne0  48563  map0cor  48568  elsetrecslem  48791  alimp-no-surprise  48875