Theorem imnan 400

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

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

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 397

This theorem is referenced by:  imnani  401  iman  402  mpnanrd  410  nan  827  ianor  979  pm5.17  1009  pm5.16  1011  dn1  1055  dfnan2  1489  nic-ax  1676  nic-axALT  1677  imnang  1845  dfsb3  2499  ralinexa  3192  pssn2lp  4037  indifdi  4218  disj  4382  disjOLD  4383  disjsn  4648  sotric  5532  poirr2  6034  ordtri1  6303  funun  6487  imadif  6525  brprcneu  6773  brprcneuALT  6774  soisoi  7208  ordsucss  7674  ordunisuc2  7700  oalimcl  8400  omlimcl  8418  unblem1  9075  suppr  9239  infpr  9271  cantnfp1lem3  9447  alephnbtwn  9836  kmlem4  9918  cfsuc  10022  isf32lem5  10122  hargch  10438  xrltnsym2  12881  fzp1nel  13349  fsumsplit  15462  sumsplit  15489  phiprmpw  16486  odzdvds  16505  pcdvdsb  16579  prmreclem5  16630  ramlb  16729  pltn2lp  18068  gsumzsplit  19537  dprdcntz2  19650  lbsextlem4  20432  obselocv  20944  maducoeval2  21798  lmmo  22540  kqcldsat  22893  rnelfmlem  23112  tsmssplit  23312  itg2splitlem  24922  itg2split  24923  fsumharmonic  26170  lgsne0  26492  lgsquadlem3  26539  2sqcoprm  26592  axtgupdim2  26841  nmounbi  29147  hatomistici  30733  nelbOLDOLD  30826  eliccelico  31107  elicoelioo  31108  nn0min  31143  isarchi2  31448  archiabl  31461  oddpwdc  32330  eulerpartlemsv2  32334  eulerpartlems  32336  eulerpartlemv  32340  eulerpartlemgh  32354  eulerpartlemgs2  32356  ballotlemfrcn0  32505  bnj1533  32841  bnj1204  33001  bnj1280  33009  subfacp1lem6  33156  poseq  33811  wzel  33827  nosepssdm  33898  nosupbnd1lem4  33923  noinfbnd1lem4  33938  nocvxminlem  33981  df3nandALT1  34597  df3nandALT2  34598  limsucncmpi  34643  unblimceq0  34696  relowlpssretop  35544  pibt2  35597  nninfnub  35918  atlatmstc  37340  sn-dtru  40195  fnwe2lem2  40883  dfxor4  41381  pm10.57  41996  limclner  43199  limsupub  43252  limsuppnflem  43258  limsupre2lem  43272  icccncfext  43435  stoweidlem14  43562  stoweidlem34  43582  stoweidlem44  43592  ldepslinc  45861  fdomne0  46188  map0cor  46193  elsetrecslem  46415  alimp-no-surprise  46496