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

Theorem imnan 437
 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 385 . 2 ((𝜑𝜓) ↔ ¬ (𝜑 → ¬ 𝜓))
21con2bii 346 1 ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑𝜓))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383 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 196  df-an 385 This theorem is referenced by:  imnani  438  iman  439  ianor  508  nan  602  pm5.17  928  pm5.16  930  dn1  1000  nannan  1443  nic-ax  1589  nic-axALT  1590  imnang  1758  dfsb3  2362  ralinexa  2980  pssn2lp  3670  disj  3969  minelOLD  3986  disjsn  4192  sotric  4985  poirr2  5439  ordtri1  5673  funun  5846  imadif  5887  brprcneu  6096  soisoi  6478  ordsucss  6910  ordunisuc2  6936  oalimcl  7527  omlimcl  7545  unblem1  8097  suppr  8260  infpr  8292  cantnfp1lem3  8460  alephnbtwn  8777  kmlem4  8858  cfsuc  8962  isf32lem5  9062  hargch  9374  xrltnsym2  11847  fzp1nel  12293  fsumsplit  14318  sumsplit  14341  phiprmpw  15319  odzdvds  15338  pcdvdsb  15411  prmreclem5  15462  ramlb  15561  pltn2lp  16792  gsumzsplit  18150  dprdcntz2  18260  lbsextlem4  18982  obselocv  19891  maducoeval2  20265  lmmo  20994  kqcldsat  21346  rnelfmlem  21566  tsmssplit  21765  itg2splitlem  23321  itg2split  23322  fsumharmonic  24538  lgsne0  24860  lgsquadlem3  24907  axtgupdim2  25170  nmounbi  27015  hatomistici  28605  eliccelico  28929  elicoelioo  28930  nn0min  28954  2sqcoprm  28978  isarchi2  29070  archiabl  29083  oddpwdc  29743  eulerpartlemsv2  29747  eulerpartlems  29749  eulerpartlemv  29753  eulerpartlemgh  29767  eulerpartlemgs2  29769  ballotlemfrcn0  29918  bnj1533  30176  bnj1204  30334  bnj1280  30342  subfacp1lem6  30421  poseq  30994  wzel  31015  wzelOLD  31016  nodenselem5  31084  nodenselem7  31086  nocvxminlem  31089  nofulllem5  31105  df3nandALT1  31566  df3nandALT2  31567  limsucncmpi  31614  unblimceq0  31668  mpnanrd  32354  relowlpssretop  32388  wl-dfnan2  32475  nninfnub  32717  atlatmstc  33624  fnwe2lem2  36639  dfxor4  37077  pm10.57  37592  limclner  38718  icccncfext  38773  stoweidlem14  38907  stoweidlem34  38927  stoweidlem44  38937  ldepslinc  42092  elsetrecslem  42243  alimp-no-surprise  42336
 Copyright terms: Public domain W3C validator