Theorem imnan 398

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

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

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 395

This theorem is referenced by:  imnani  399  iman  400  mpnanrd  408  nan  828  ianor  979  pm5.17  1009  pm5.16  1011  dn1  1055  dfnan2  1488  nic-ax  1668  nic-axALT  1669  imnang  1837  dfsb3  2488  ralinexa  3091  pssn2lp  4100  indifdi  4285  disj  4452  disjOLD  4453  disjsn  4720  sotric  5622  poirr2  6136  ordtri1  6409  funun  6605  imadif  6643  brprcneu  6891  brprcneuALT  6892  soisoi  7340  ordsucss  7827  ordunisuc2  7854  poseq  8172  oalimcl  8590  omlimcl  8608  unblem1  9329  suppr  9514  infpr  9546  cantnfp1lem3  9723  alephnbtwn  10114  kmlem4  10196  cfsuc  10300  isf32lem5  10400  hargch  10716  xrltnsym2  13171  fzp1nel  13639  fsumsplit  15745  sumsplit  15772  phiprmpw  16778  odzdvds  16797  pcdvdsb  16871  prmreclem5  16922  ramlb  17021  pltn2lp  18366  gsumzsplit  19925  dprdcntz2  20038  lbsextlem4  21142  obselocv  21726  psdmul  22160  maducoeval2  22633  lmmo  23375  kqcldsat  23728  rnelfmlem  23947  tsmssplit  24147  itg2splitlem  25769  itg2split  25770  fsumharmonic  27040  lgsne0  27364  lgsquadlem3  27411  2sqcoprm  27464  nosepssdm  27716  nosupbnd1lem4  27741  noinfbnd1lem4  27756  nocvxminlem  27807  axtgupdim2  28398  nmounbi  30709  hatomistici  32295  eliccelico  32679  elicoelioo  32680  nn0difffzod  32708  nn0min  32721  isarchi2  33050  archiabl  33063  oddpwdc  34188  eulerpartlemsv2  34192  eulerpartlems  34194  eulerpartlemv  34198  eulerpartlemgh  34212  eulerpartlemgs2  34214  ballotlemfrcn0  34363  bnj1533  34697  bnj1204  34857  bnj1280  34865  subfacp1lem6  35013  wzel  35648  df3nandALT1  36111  df3nandALT2  36112  limsucncmpi  36157  unblimceq0  36210  relowlpssretop  37071  pibt2  37124  nninfnub  37452  atlatmstc  39017  fnwe2lem2  42712  dfxor4  43433  pm10.57  44045  limclner  45272  limsupub  45325  limsuppnflem  45331  limsupre2lem  45345  icccncfext  45508  stoweidlem14  45635  stoweidlem34  45655  stoweidlem44  45665  ldepslinc  47892  fdomne0  48217  map0cor  48222  elsetrecslem  48445  alimp-no-surprise  48529