MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imnan Structured version   Visualization version   GIF version

Theorem imnan 400
Description: Express an implication in terms of a negated conjunction. (Contributed by NM, 9-Apr-1994.)
Assertion
Ref Expression
imnan ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑𝜓))

Proof of Theorem imnan
StepHypRef Expression
1 df-an 397 . 2 ((𝜑𝜓) ↔ ¬ (𝜑 → ¬ 𝜓))
21con2bii 359 1 ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396
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 208  df-an 397
This theorem is referenced by:  imnani  401  iman  402  mpnanrd  410  nan  825  ianor  975  pm5.17  1005  pm5.16  1007  dn1  1049  nanimn  1478  nic-ax  1665  nic-axALT  1666  imnang  1833  dfsb3  2529  dfsb3ALT  2588  ralinexa  3264  pssn2lp  4077  disj  4397  disjsn  4641  sotric  5495  poirr2  5978  ordtri1  6218  funun  6394  imadif  6432  brprcneu  6656  soisoi  7070  ordsucss  7521  ordunisuc2  7547  oalimcl  8176  omlimcl  8194  unblem1  8759  suppr  8924  infpr  8956  cantnfp1lem3  9132  alephnbtwn  9486  kmlem4  9568  cfsuc  9668  isf32lem5  9768  hargch  10084  xrltnsym2  12521  fzp1nel  12981  fsumsplit  15087  sumsplit  15113  phiprmpw  16103  odzdvds  16122  pcdvdsb  16195  prmreclem5  16246  ramlb  16345  pltn2lp  17569  gsumzsplit  18978  dprdcntz2  19091  lbsextlem4  19864  obselocv  20802  maducoeval2  21179  lmmo  21918  kqcldsat  22271  rnelfmlem  22490  tsmssplit  22689  itg2splitlem  24278  itg2split  24279  fsumharmonic  25517  lgsne0  25839  lgsquadlem3  25886  2sqcoprm  25939  axtgupdim2  26185  nmounbi  28481  hatomistici  30067  nelbOLD  30160  eliccelico  30427  elicoelioo  30428  nn0min  30464  isarchi2  30742  archiabl  30755  oddpwdc  31512  eulerpartlemsv2  31516  eulerpartlems  31518  eulerpartlemv  31522  eulerpartlemgh  31536  eulerpartlemgs2  31538  ballotlemfrcn0  31687  bnj1533  32024  bnj1204  32182  bnj1280  32190  subfacp1lem6  32330  poseq  32993  wzel  33009  nosepssdm  33088  nosupbnd1lem4  33109  nocvxminlem  33145  df3nandALT1  33645  df3nandALT2  33646  limsucncmpi  33691  unblimceq0  33744  relowlpssretop  34528  pibt2  34581  nninfnub  34909  atlatmstc  36337  sn-dtru  38991  fnwe2lem2  39531  dfxor4  39991  pm10.57  40583  limclner  41812  limsupub  41865  limsuppnflem  41871  limsupre2lem  41885  icccncfext  42050  stoweidlem14  42180  stoweidlem34  42200  stoweidlem44  42210  ldepslinc  44462  elsetrecslem  44699  alimp-no-surprise  44780
  Copyright terms: Public domain W3C validator