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  2528  ralinexa  3120  pssn2lp  4060  indifdi  4247  disj  4410  disjsn  4679  sotric  5601  poirr2  6126  ordtri1  6398  funun  6586  imadif  6624  brprcneu  6875  brprcneuALT  6876  soisoi  7335  ordsucss  7820  ordunisuc2  7846  poseq  8160  oalimcl  8551  omlimcl  8569  unblem1  9259  suppr  9439  infpr  9472  nelaneqOLD  9572  cantnfp1lem3  9656  alephnbtwn  10071  kmlem4  10153  cfsuc  10256  isf32lem5  10356  hargch  10675  xrltnsym2  13181  fzp1nel  13658  fsumsplit  15817  sumsplit  15844  phiprmpw  16859  odzdvds  16879  pcdvdsb  16953  prmreclem5  17004  ramlb  17103  pltn2lp  18419  gsumzsplit  20043  dprdcntz2  20156  lbsextlem4  21337  obselocv  21930  psdmul  22381  maducoeval2  22849  lmmo  23589  kqcldsat  23943  rnelfmlem  24162  tsmssplit  24362  itg2splitlem  25960  itg2split  25961  fsumharmonic  27229  lgsne0  27552  lgsquadlem3  27599  2sqcoprm  27652  nosepssdm  27903  nosupbnd1lem4  27928  noinfbnd1lem4  27943  nocvxminlem  28000  bdayfinbndlem1  28713  axtgupdim2  28793  nmounbi  31201  hatomistici  32787  eliccelico  33194  elicoelioo  33195  nn0difffzod  33221  nn0min  33237  isarchi2  33571  archiabl  33584  extdgfialglem1  34148  oddpwdc  34811  eulerpartlemsv2  34815  eulerpartlems  34817  eulerpartlemv  34821  eulerpartlemgh  34835  eulerpartlemgs2  34837  ballotlemfrcn0  34987  bnj1533  35307  bnj1204  35467  bnj1280  35475  xoromon  35539  fineqvinfep  35597  subfacp1lem6  35716  wzel  36353  df3nandALT1  36969  df3nandALT2  36970  limsucncmpi  37015  weiunfr  37037  regsfromregtco  37108  unblimceq0  37155  bj-axseprep  37770  relowlpssretop  38069  pibt2  38122  nninfnub  38462  atlatmstc  40153  fnwe2lem2  43838  dfxor4  44552  pm10.57  45141  limclner  46425  limsupub  46478  limsuppnflem  46484  limsupre2lem  46498  icccncfext  46661  stoweidlem14  46788  stoweidlem34  46808  stoweidlem44  46818  ldepslinc  49348  fdomne0  49687  map0cor  49692  elsetrecslem  50536  alimp-no-surprise  50618