Theorem imnan 401

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

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

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 398

This theorem is referenced by:  imnani  402  iman  403  mpnanrd  411  nan  829  ianor  981  pm5.17  1011  pm5.16  1013  dn1  1057  dfnan2  1493  nic-ax  1676  nic-axALT  1677  imnang  1845  dfsb3  2494  ralinexa  3102  pssn2lp  4101  indifdi  4283  disj  4447  disjOLD  4448  disjsn  4715  sotric  5616  poirr2  6123  ordtri1  6395  funun  6592  imadif  6630  brprcneu  6879  brprcneuALT  6880  soisoi  7322  ordsucss  7803  ordunisuc2  7830  poseq  8141  oalimcl  8557  omlimcl  8575  unblem1  9292  suppr  9463  infpr  9495  cantnfp1lem3  9672  alephnbtwn  10063  kmlem4  10145  cfsuc  10249  isf32lem5  10349  hargch  10665  xrltnsym2  13114  fzp1nel  13582  fsumsplit  15684  sumsplit  15711  phiprmpw  16706  odzdvds  16725  pcdvdsb  16799  prmreclem5  16850  ramlb  16949  pltn2lp  18291  gsumzsplit  19790  dprdcntz2  19903  lbsextlem4  20767  obselocv  21275  maducoeval2  22134  lmmo  22876  kqcldsat  23229  rnelfmlem  23448  tsmssplit  23648  itg2splitlem  25258  itg2split  25259  fsumharmonic  26506  lgsne0  26828  lgsquadlem3  26875  2sqcoprm  26928  nosepssdm  27179  nosupbnd1lem4  27204  noinfbnd1lem4  27219  nocvxminlem  27269  axtgupdim2  27712  nmounbi  30017  hatomistici  31603  eliccelico  31976  elicoelioo  31977  nn0difffzod  32004  nn0min  32014  isarchi2  32319  archiabl  32332  oddpwdc  33342  eulerpartlemsv2  33346  eulerpartlems  33348  eulerpartlemv  33352  eulerpartlemgh  33366  eulerpartlemgs2  33368  ballotlemfrcn0  33517  bnj1533  33852  bnj1204  34012  bnj1280  34020  subfacp1lem6  34165  wzel  34785  df3nandALT1  35273  df3nandALT2  35274  limsucncmpi  35319  unblimceq0  35372  relowlpssretop  36234  pibt2  36287  nninfnub  36608  atlatmstc  38178  fnwe2lem2  41779  dfxor4  42503  pm10.57  43116  limclner  44354  limsupub  44407  limsuppnflem  44413  limsupre2lem  44427  icccncfext  44590  stoweidlem14  44717  stoweidlem34  44737  stoweidlem44  44747  ldepslinc  47144  fdomne0  47470  map0cor  47475  elsetrecslem  47698  alimp-no-surprise  47782