Theorem imnan 388

Description: Express implication in terms of conjunction. (Contributed by NM, 9-Apr-1994.)

Assertion

Ref	Expression
imnan	⊢ ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓))

Proof of Theorem imnan

Step	Hyp	Ref	Expression
1		df-an 385	. 2 ⊢ ((𝜑 ∧ 𝜓) ↔ ¬ (𝜑 → ¬ 𝜓))
2	1	con2bii 348	1 ⊢ ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 197   ∧ wa 384

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 198  df-an 385

This theorem is referenced by:  imnani  389  iman  390  nan  850  ianor  995  pm5.17  1026  pm5.16  1028  dn1  1073  nannan  1605  nic-ax  1753  nic-axALT  1754  imnang  1928  dfsb3  2533  ralinexa  3184  pssn2lp  3906  disj  4214  disjsn  4438  sotric  5258  poirr2  5731  ordtri1  5969  funun  6146  imadif  6184  brprcneu  6400  soisoi  6802  ordsucss  7248  ordunisuc2  7274  oalimcl  7877  omlimcl  7895  unblem1  8451  suppr  8616  infpr  8648  cantnfp1lem3  8824  alephnbtwn  9177  kmlem4  9260  cfsuc  9364  isf32lem5  9464  hargch  9780  xrltnsym2  12187  fzp1nel  12647  fsumsplit  14694  sumsplit  14722  phiprmpw  15698  odzdvds  15717  pcdvdsb  15790  prmreclem5  15841  ramlb  15940  pltn2lp  17174  gsumzsplit  18528  dprdcntz2  18639  lbsextlem4  19370  obselocv  20282  maducoeval2  20657  lmmo  21398  kqcldsat  21750  rnelfmlem  21969  tsmssplit  22168  itg2splitlem  23729  itg2split  23730  fsumharmonic  24952  lgsne0  25274  lgsquadlem3  25321  axtgupdim2  25584  nmounbi  27959  hatomistici  29549  eliccelico  29866  elicoelioo  29867  nn0min  29894  2sqcoprm  29972  isarchi2  30064  archiabl  30077  oddpwdc  30741  eulerpartlemsv2  30745  eulerpartlems  30747  eulerpartlemv  30751  eulerpartlemgh  30765  eulerpartlemgs2  30767  ballotlemfrcn0  30916  bnj1533  31245  bnj1204  31403  bnj1280  31411  subfacp1lem6  31490  poseq  32074  wzel  32090  nosepssdm  32157  nosupbnd1lem4  32178  nocvxminlem  32214  df3nandALT1  32715  df3nandALT2  32716  limsucncmpi  32761  unblimceq0  32815  mpnanrd  33495  relowlpssretop  33528  wl-dfnan2  33612  nninfnub  33858  atlatmstc  35099  fnwe2lem2  38122  dfxor4  38558  pm10.57  39070  limclner  40363  limsupub  40416  limsuppnflem  40422  limsupre2lem  40436  icccncfext  40580  stoweidlem14  40710  stoweidlem34  40730  stoweidlem44  40740  ldepslinc  42866  elsetrecslem  43013  alimp-no-surprise  43098