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

Theorem imnan 436
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 384 . 2 ((𝜑𝜓) ↔ ¬ (𝜑 → ¬ 𝜓))
21con2bii 345 1 ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wa 382
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 195  df-an 384
This theorem is referenced by:  imnani  437  iman  438  ianor  507  nan  601  pm5.17  927  pm5.16  929  dn1  999  nannan  1442  nic-ax  1588  nic-axALT  1589  imnang  1757  dfsb3  2361  ralinexa  2979  pssn2lp  3669  disj  3968  minelOLD  3985  disjsn  4191  sotric  4975  poirr2  5426  ordtri1  5659  funun  5832  imadif  5873  brprcneu  6081  soisoi  6456  ordsucss  6888  ordunisuc2  6914  oalimcl  7505  omlimcl  7523  unblem1  8075  suppr  8238  infpr  8270  cantnfp1lem3  8438  alephnbtwn  8755  kmlem4  8836  cfsuc  8940  isf32lem5  9040  hargch  9352  xrltnsym2  11809  fzp1nel  12251  fsumsplit  14267  sumsplit  14290  phiprmpw  15268  odzdvds  15287  pcdvdsb  15360  prmreclem5  15411  ramlb  15510  pltn2lp  16741  gsumzsplit  18099  dprdcntz2  18209  lbsextlem4  18931  obselocv  19839  maducoeval2  20213  lmmo  20942  kqcldsat  21294  rnelfmlem  21514  tsmssplit  21713  itg2splitlem  23266  itg2split  23267  fsumharmonic  24483  lgsne0  24805  lgsquadlem3  24852  axtgupdim2  25115  nmounbi  26849  hatomistici  28439  eliccelico  28763  elicoelioo  28764  nn0min  28788  2sqcoprm  28812  isarchi2  28904  archiabl  28917  oddpwdc  29577  eulerpartlemsv2  29581  eulerpartlems  29583  eulerpartlemv  29587  eulerpartlemgh  29601  eulerpartlemgs2  29603  ballotlemfrcn0  29752  bnj1533  30010  bnj1204  30168  bnj1280  30176  subfacp1lem6  30255  poseq  30828  wzel  30849  wzelOLD  30850  nodenselem5  30918  nodenselem7  30920  nocvxminlem  30923  nofulllem5  30939  df3nandALT1  31400  df3nandALT2  31401  limsucncmpi  31448  unblimceq0  31502  mpnanrd  32178  relowlpssretop  32212  wl-dfnan2  32299  nninfnub  32541  atlatmstc  33448  fnwe2lem2  36463  dfxor4  36901  pm10.57  37416  limclner  38542  icccncfext  38597  stoweidlem14  38731  stoweidlem34  38751  stoweidlem44  38761  ldepslinc  42114  alimp-no-surprise  42319
  Copyright terms: Public domain W3C validator