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

Theorem imnan 403
 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 400 . 2 ((𝜑𝜓) ↔ ¬ (𝜑 → ¬ 𝜓))
21con2bii 361 1 ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑𝜓))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399 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 210  df-an 400 This theorem is referenced by:  imnani  404  iman  405  mpnanrd  413  nan  828  ianor  979  pm5.17  1009  pm5.16  1011  dn1  1053  nanimn  1485  nic-ax  1675  nic-axALT  1676  imnang  1843  dfsb3  2515  dfsb3ALT  2571  ralinexa  3226  pssn2lp  4032  disj  4358  disjOLD  4359  disjsn  4610  sotric  5469  poirr2  5955  ordtri1  6196  funun  6374  imadif  6412  brprcneu  6641  soisoi  7064  ordsucss  7517  ordunisuc2  7543  oalimcl  8173  omlimcl  8191  unblem1  8758  suppr  8923  infpr  8955  cantnfp1lem3  9131  alephnbtwn  9486  kmlem4  9568  cfsuc  9672  isf32lem5  9772  hargch  10088  xrltnsym2  12523  fzp1nel  12990  fsumsplit  15092  sumsplit  15118  phiprmpw  16106  odzdvds  16125  pcdvdsb  16198  prmreclem5  16249  ramlb  16348  pltn2lp  17574  gsumzsplit  19043  dprdcntz2  19156  lbsextlem4  19929  obselocv  20420  maducoeval2  21248  lmmo  21988  kqcldsat  22341  rnelfmlem  22560  tsmssplit  22760  itg2splitlem  24355  itg2split  24356  fsumharmonic  25600  lgsne0  25922  lgsquadlem3  25969  2sqcoprm  26022  axtgupdim2  26268  nmounbi  28562  hatomistici  30148  nelbOLD  30242  eliccelico  30529  elicoelioo  30530  nn0min  30565  isarchi2  30867  archiabl  30880  oddpwdc  31720  eulerpartlemsv2  31724  eulerpartlems  31726  eulerpartlemv  31730  eulerpartlemgh  31744  eulerpartlemgs2  31746  ballotlemfrcn0  31895  bnj1533  32232  bnj1204  32392  bnj1280  32400  subfacp1lem6  32540  poseq  33203  wzel  33219  nosepssdm  33298  nosupbnd1lem4  33319  nocvxminlem  33355  df3nandALT1  33855  df3nandALT2  33856  limsucncmpi  33901  unblimceq0  33954  relowlpssretop  34776  pibt2  34829  nninfnub  35182  atlatmstc  36608  sn-dtru  39390  fnwe2lem2  39982  dfxor4  40454  pm10.57  41062  limclner  42280  limsupub  42333  limsuppnflem  42339  limsupre2lem  42353  icccncfext  42516  stoweidlem14  42643  stoweidlem34  42663  stoweidlem44  42673  ldepslinc  44905  elsetrecslem  45215  alimp-no-surprise  45296
 Copyright terms: Public domain W3C validator