Theorem imnan 405

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  imnani  406  iman  407  mpnanrd  415  nan  843  ianor  997  pm5.17  1029  pm5.16  1031  dn1  1073  dfnan2  1524  nic-ax  1706  nic-axALT  1707  imnang  1875  dfsb3  2526  ralinexa  3119  pssn2lp  4035  indifdi  4242  disj  4406  disjsn  4673  sotric  5596  poirr2  6136  ordtri1  6422  funun  6614  imadif  6654  brprcneu  6906  brprcneuALT  6907  soisoi  7367  ordsucss  7863  ordunisuc2  7889  fnwe2lem3  8184  poseq  8212  oalimcl  8606  omlimcl  8624  unblem1  9322  suppr  9501  infpr  9534  nelaneqOLD  9634  cantnfp1lem3  9718  alephnbtwn  10189  kmlem4  10271  cfsuc  10374  isf32lem5  10474  hargch  10797  xrltnsym2  13307  fzp1nel  13785  fsumsplit  15951  sumsplit  15978  phiprmpw  16997  odzdvds  17017  pcdvdsb  17091  prmreclem5  17142  ramlb  17241  pltn2lp  18563  gsumzsplit  20192  dprdcntz2  20305  lbsextlem4  21490  obselocv  22089  psdmul  22542  maducoeval2  23010  lmmo  23753  kqcldsat  24107  rnelfmlem  24326  tsmssplit  24526  itg2splitlem  26124  itg2split  26125  fsumharmonic  27396  lgsne0  27719  lgsquadlem3  27766  2sqcoprm  27819  nosepssdm  28100  nosupbnd1lem4  28125  noinfbnd1lem4  28140  nocvxminlem  28197  bdayfinbndlem1  28910  axtgupdim2  28990  nmounbi  31435  hatomistici  33021  eliccelico  33465  elicoelioo  33466  nn0difffzod  33492  nn0min  33508  isarchi2  33845  archiabl  33858  extdgfialglem1  34435  oddpwdc  35097  eulerpartlemsv2  35101  eulerpartlems  35103  eulerpartlemv  35107  eulerpartlemgh  35121  eulerpartlemgs2  35123  ballotlemfrcn0  35273  bnj1533  35593  bnj1204  35753  bnj1280  35761  xoromon  35835  fineqvinfep  35934  subfacp1lem6  36158  wzel  36801  df3nandALT1  37402  df3nandALT2  37403  limsucncmpi  37448  weiunfr  37470  regsfromregtco  37541  unblimceq0  37588  bj-axseprep  38260  relowlpssretop  38555  pibt2  38608  nninfnub  38951  atlatmstc  40642  dfxor4  45027  pm10.57  45616  limclner  46934  limsupub  46987  limsuppnflem  46993  limsupre2lem  47007  icccncfext  47170  stoweidlem14  47297  stoweidlem34  47317  stoweidlem44  47327  ldepslinc  49952  fdomne0  50292  map0cor  50297  elsetrecslem  51198  alimp-no-surprise  51305