Theorem imnan 402

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  imnani  403  iman  404  mpnanrd  412  nan  827  ianor  978  pm5.17  1008  pm5.16  1010  dn1  1052  nanimn  1484  nic-ax  1674  nic-axALT  1675  imnang  1842  dfsb3  2533  dfsb3ALT  2592  ralinexa  3264  pssn2lp  4078  disj  4399  disjsn  4647  sotric  5501  poirr2  5984  ordtri1  6224  funun  6400  imadif  6438  brprcneu  6662  soisoi  7081  ordsucss  7533  ordunisuc2  7559  oalimcl  8186  omlimcl  8204  unblem1  8770  suppr  8935  infpr  8967  cantnfp1lem3  9143  alephnbtwn  9497  kmlem4  9579  cfsuc  9679  isf32lem5  9779  hargch  10095  xrltnsym2  12532  fzp1nel  12992  fsumsplit  15097  sumsplit  15123  phiprmpw  16113  odzdvds  16132  pcdvdsb  16205  prmreclem5  16256  ramlb  16355  pltn2lp  17579  gsumzsplit  19047  dprdcntz2  19160  lbsextlem4  19933  obselocv  20872  maducoeval2  21249  lmmo  21988  kqcldsat  22341  rnelfmlem  22560  tsmssplit  22760  itg2splitlem  24349  itg2split  24350  fsumharmonic  25589  lgsne0  25911  lgsquadlem3  25958  2sqcoprm  26011  axtgupdim2  26257  nmounbi  28553  hatomistici  30139  nelbOLD  30232  eliccelico  30500  elicoelioo  30501  nn0min  30536  isarchi2  30814  archiabl  30827  oddpwdc  31612  eulerpartlemsv2  31616  eulerpartlems  31618  eulerpartlemv  31622  eulerpartlemgh  31636  eulerpartlemgs2  31638  ballotlemfrcn0  31787  bnj1533  32124  bnj1204  32284  bnj1280  32292  subfacp1lem6  32432  poseq  33095  wzel  33111  nosepssdm  33190  nosupbnd1lem4  33211  nocvxminlem  33247  df3nandALT1  33747  df3nandALT2  33748  limsucncmpi  33793  unblimceq0  33846  relowlpssretop  34648  pibt2  34701  nninfnub  35041  atlatmstc  36470  sn-dtru  39131  fnwe2lem2  39671  dfxor4  40131  pm10.57  40723  limclner  41952  limsupub  42005  limsuppnflem  42011  limsupre2lem  42025  icccncfext  42190  stoweidlem14  42319  stoweidlem34  42339  stoweidlem44  42349  ldepslinc  44584  elsetrecslem  44821  alimp-no-surprise  44902