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  2499  ralinexa  3091  pssn2lp  4045  indifdi  4235  disj  4391  disjsn  4656  sotric  5563  poirr2  6082  ordtri1  6351  funun  6539  imadif  6577  brprcneu  6825  brprcneuALT  6826  soisoi  7277  ordsucss  7763  ordunisuc2  7789  poseq  8102  oalimcl  8489  omlimcl  8507  unblem1  9196  suppr  9379  infpr  9412  nelaneqOLD  9511  cantnfp1lem3  9595  alephnbtwn  9987  kmlem4  10070  cfsuc  10173  isf32lem5  10273  hargch  10590  xrltnsym2  13083  fzp1nel  13559  fsumsplit  15697  sumsplit  15724  phiprmpw  16740  odzdvds  16760  pcdvdsb  16834  prmreclem5  16885  ramlb  16984  pltn2lp  18299  gsumzsplit  19896  dprdcntz2  20009  lbsextlem4  21154  obselocv  21721  psdmul  22145  maducoeval2  22618  lmmo  23358  kqcldsat  23711  rnelfmlem  23930  tsmssplit  24130  itg2splitlem  25728  itg2split  25729  fsumharmonic  26992  lgsne0  27315  lgsquadlem3  27362  2sqcoprm  27415  nosepssdm  27667  nosupbnd1lem4  27692  noinfbnd1lem4  27707  nocvxminlem  27763  bdayfinbndlem1  28476  axtgupdim2  28556  nmounbi  30865  hatomistici  32451  eliccelico  32868  elicoelioo  32869  nn0difffzod  32895  nn0min  32912  isarchi2  33264  archiabl  33277  extdgfialglem1  33855  oddpwdc  34517  eulerpartlemsv2  34521  eulerpartlems  34523  eulerpartlemv  34527  eulerpartlemgh  34541  eulerpartlemgs2  34543  ballotlemfrcn0  34693  bnj1533  35013  bnj1204  35173  bnj1280  35181  xoromon  35251  fineqvinfep  35288  subfacp1lem6  35386  wzel  36023  df3nandALT1  36600  df3nandALT2  36601  limsucncmpi  36646  weiunfr  36668  regsfromregtco  36739  unblimceq0  36786  bj-axseprep  37400  relowlpssretop  37697  pibt2  37750  nninfnub  38089  atlatmstc  39782  fnwe2lem2  43500  dfxor4  44214  pm10.57  44819  limclner  46100  limsupub  46153  limsuppnflem  46159  limsupre2lem  46173  icccncfext  46336  stoweidlem14  46463  stoweidlem34  46483  stoweidlem44  46493  ldepslinc  49000  fdomne0  49340  map0cor  49345  elsetrecslem  50189  alimp-no-surprise  50271