Theorem imnan 401

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  imnani  402  iman  403  mpnanrd  411  nan  829  ianor  981  pm5.17  1011  pm5.16  1013  dn1  1057  dfnan2  1493  nic-ax  1676  nic-axALT  1677  imnang  1845  dfsb3  2494  ralinexa  3102  pssn2lp  4102  indifdi  4284  disj  4448  disjOLD  4449  disjsn  4716  sotric  5617  poirr2  6126  ordtri1  6398  funun  6595  imadif  6633  brprcneu  6882  brprcneuALT  6883  soisoi  7325  ordsucss  7806  ordunisuc2  7833  poseq  8144  oalimcl  8560  omlimcl  8578  unblem1  9295  suppr  9466  infpr  9498  cantnfp1lem3  9675  alephnbtwn  10066  kmlem4  10148  cfsuc  10252  isf32lem5  10352  hargch  10668  xrltnsym2  13117  fzp1nel  13585  fsumsplit  15687  sumsplit  15714  phiprmpw  16709  odzdvds  16728  pcdvdsb  16802  prmreclem5  16853  ramlb  16952  pltn2lp  18294  gsumzsplit  19795  dprdcntz2  19908  lbsextlem4  20774  obselocv  21283  maducoeval2  22142  lmmo  22884  kqcldsat  23237  rnelfmlem  23456  tsmssplit  23656  itg2splitlem  25266  itg2split  25267  fsumharmonic  26516  lgsne0  26838  lgsquadlem3  26885  2sqcoprm  26938  nosepssdm  27189  nosupbnd1lem4  27214  noinfbnd1lem4  27229  nocvxminlem  27279  axtgupdim2  27753  nmounbi  30060  hatomistici  31646  eliccelico  32019  elicoelioo  32020  nn0difffzod  32047  nn0min  32057  isarchi2  32362  archiabl  32375  oddpwdc  33384  eulerpartlemsv2  33388  eulerpartlems  33390  eulerpartlemv  33394  eulerpartlemgh  33408  eulerpartlemgs2  33410  ballotlemfrcn0  33559  bnj1533  33894  bnj1204  34054  bnj1280  34062  subfacp1lem6  34207  wzel  34827  df3nandALT1  35332  df3nandALT2  35333  limsucncmpi  35378  unblimceq0  35431  relowlpssretop  36293  pibt2  36346  nninfnub  36667  atlatmstc  38237  fnwe2lem2  41841  dfxor4  42565  pm10.57  43178  limclner  44415  limsupub  44468  limsuppnflem  44474  limsupre2lem  44488  icccncfext  44651  stoweidlem14  44778  stoweidlem34  44798  stoweidlem44  44808  ldepslinc  47238  fdomne0  47564  map0cor  47569  elsetrecslem  47792  alimp-no-surprise  47876