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  1494  nic-ax  1673  nic-axALT  1674  imnang  1842  dfsb3  2499  ralinexa  3101  pssn2lp  4104  indifdi  4294  disj  4450  disjsn  4711  sotric  5622  poirr2  6144  ordtri1  6417  funun  6612  imadif  6650  brprcneu  6896  brprcneuALT  6897  soisoi  7348  ordsucss  7838  ordunisuc2  7865  poseq  8183  oalimcl  8598  omlimcl  8616  unblem1  9328  suppr  9511  infpr  9543  cantnfp1lem3  9720  alephnbtwn  10111  kmlem4  10194  cfsuc  10297  isf32lem5  10397  hargch  10713  xrltnsym2  13180  fzp1nel  13651  fsumsplit  15777  sumsplit  15804  phiprmpw  16813  odzdvds  16833  pcdvdsb  16907  prmreclem5  16958  ramlb  17057  pltn2lp  18386  gsumzsplit  19945  dprdcntz2  20058  lbsextlem4  21163  obselocv  21748  psdmul  22170  maducoeval2  22646  lmmo  23388  kqcldsat  23741  rnelfmlem  23960  tsmssplit  24160  itg2splitlem  25783  itg2split  25784  fsumharmonic  27055  lgsne0  27379  lgsquadlem3  27426  2sqcoprm  27479  nosepssdm  27731  nosupbnd1lem4  27756  noinfbnd1lem4  27771  nocvxminlem  27822  axtgupdim2  28479  nmounbi  30795  hatomistici  32381  eliccelico  32779  elicoelioo  32780  nn0difffzod  32808  nn0min  32822  isarchi2  33192  archiabl  33205  oddpwdc  34356  eulerpartlemsv2  34360  eulerpartlems  34362  eulerpartlemv  34366  eulerpartlemgh  34380  eulerpartlemgs2  34382  ballotlemfrcn0  34532  bnj1533  34866  bnj1204  35026  bnj1280  35034  subfacp1lem6  35190  wzel  35825  df3nandALT1  36400  df3nandALT2  36401  limsucncmpi  36446  weiunfr  36468  unblimceq0  36508  relowlpssretop  37365  pibt2  37418  nninfnub  37758  atlatmstc  39320  fnwe2lem2  43063  dfxor4  43779  pm10.57  44390  limclner  45666  limsupub  45719  limsuppnflem  45725  limsupre2lem  45739  icccncfext  45902  stoweidlem14  46029  stoweidlem34  46049  stoweidlem44  46059  ldepslinc  48426  fdomne0  48759  map0cor  48764  elsetrecslem  49218  alimp-no-surprise  49300