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  2493  ralinexa  3084  pssn2lp  4070  indifdi  4260  disj  4416  disjsn  4678  sotric  5579  poirr2  6100  ordtri1  6368  funun  6565  imadif  6603  brprcneu  6851  brprcneuALT  6852  soisoi  7306  ordsucss  7796  ordunisuc2  7823  poseq  8140  oalimcl  8527  omlimcl  8545  unblem1  9246  suppr  9430  infpr  9463  cantnfp1lem3  9640  alephnbtwn  10031  kmlem4  10114  cfsuc  10217  isf32lem5  10317  hargch  10633  xrltnsym2  13105  fzp1nel  13579  fsumsplit  15714  sumsplit  15741  phiprmpw  16753  odzdvds  16773  pcdvdsb  16847  prmreclem5  16898  ramlb  16997  pltn2lp  18307  gsumzsplit  19864  dprdcntz2  19977  lbsextlem4  21078  obselocv  21644  psdmul  22060  maducoeval2  22534  lmmo  23274  kqcldsat  23627  rnelfmlem  23846  tsmssplit  24046  itg2splitlem  25656  itg2split  25657  fsumharmonic  26929  lgsne0  27253  lgsquadlem3  27300  2sqcoprm  27353  nosepssdm  27605  nosupbnd1lem4  27630  noinfbnd1lem4  27645  nocvxminlem  27696  axtgupdim2  28405  nmounbi  30712  hatomistici  32298  eliccelico  32707  elicoelioo  32708  nn0difffzod  32736  nn0min  32752  isarchi2  33146  archiabl  33159  oddpwdc  34352  eulerpartlemsv2  34356  eulerpartlems  34358  eulerpartlemv  34362  eulerpartlemgh  34376  eulerpartlemgs2  34378  ballotlemfrcn0  34528  bnj1533  34849  bnj1204  35009  bnj1280  35017  subfacp1lem6  35179  wzel  35819  df3nandALT1  36394  df3nandALT2  36395  limsucncmpi  36440  weiunfr  36462  unblimceq0  36502  relowlpssretop  37359  pibt2  37412  nninfnub  37752  atlatmstc  39319  fnwe2lem2  43047  dfxor4  43762  pm10.57  44367  limclner  45656  limsupub  45709  limsuppnflem  45715  limsupre2lem  45729  icccncfext  45892  stoweidlem14  46019  stoweidlem34  46039  stoweidlem44  46049  ldepslinc  48502  fdomne0  48842  map0cor  48847  elsetrecslem  49692  alimp-no-surprise  49774