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

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

Proof of Theorem imnan
StepHypRef Expression
1 df-an 386 . 2 ((𝜑𝜓) ↔ ¬ (𝜑 → ¬ 𝜓))
21con2bii 347 1 ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  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 197  df-an 386
This theorem is referenced by:  imnani  439  iman  440  ianor  509  nan  603  pm5.17  931  pm5.16  933  dn1  1007  nannan  1448  nic-ax  1595  nic-axALT  1596  imnang  1766  dfsb3  2373  ralinexa  2993  pssn2lp  3692  disj  3995  minelOLD  4012  disjsn  4223  sotric  5031  poirr2  5489  ordtri1  5725  funun  5900  imadif  5941  brprcneu  6151  soisoi  6543  ordsucss  6980  ordunisuc2  7006  oalimcl  7600  omlimcl  7618  unblem1  8172  suppr  8337  infpr  8369  cantnfp1lem3  8537  alephnbtwn  8854  kmlem4  8935  cfsuc  9039  isf32lem5  9139  hargch  9455  xrltnsym2  11931  fzp1nel  12381  fsumsplit  14420  sumsplit  14446  phiprmpw  15424  odzdvds  15443  pcdvdsb  15516  prmreclem5  15567  ramlb  15666  pltn2lp  16909  gsumzsplit  18267  dprdcntz2  18377  lbsextlem4  19101  obselocv  20012  maducoeval2  20386  lmmo  21124  kqcldsat  21476  rnelfmlem  21696  tsmssplit  21895  itg2splitlem  23455  itg2split  23456  fsumharmonic  24672  lgsne0  24994  lgsquadlem3  25041  axtgupdim2  25304  nmounbi  27519  hatomistici  29109  eliccelico  29424  elicoelioo  29425  nn0min  29450  2sqcoprm  29474  isarchi2  29566  archiabl  29579  oddpwdc  30239  eulerpartlemsv2  30243  eulerpartlems  30245  eulerpartlemv  30249  eulerpartlemgh  30263  eulerpartlemgs2  30265  ballotlemfrcn0  30414  bnj1533  30683  bnj1204  30841  bnj1280  30849  subfacp1lem6  30928  poseq  31504  wzel  31525  wzelOLD  31526  nodenselem5  31601  nodenselem7  31603  nocvxminlem  31606  df3nandALT1  32091  df3nandALT2  32092  limsucncmpi  32139  unblimceq0  32193  mpnanrd  32849  relowlpssretop  32883  wl-dfnan2  32967  nninfnub  33218  atlatmstc  34125  fnwe2lem2  37140  dfxor4  37578  pm10.57  38091  limclner  39319  limsupub  39372  limsuppnflem  39378  limsupre2lem  39392  icccncfext  39435  stoweidlem14  39568  stoweidlem34  39588  stoweidlem44  39598  ldepslinc  41616  elsetrecslem  41767  alimp-no-surprise  41860
  Copyright terms: Public domain W3C validator