MPE Home 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 196  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 197  df-an 385
This theorem is referenced by:  imnani  438  iman  439  ianor  508  nan  603  pm5.17  950  pm5.16  952  dn1  1028  nannan  1491  nic-ax  1638  nic-axALT  1639  imnang  1809  dfsb3  2402  ralinexa  3026  pssn2lp  3741  disj  4050  minelOLD  4067  disjsn  4278  sotric  5090  poirr2  5555  ordtri1  5794  funun  5970  imadif  6011  brprcneu  6222  soisoi  6618  ordsucss  7060  ordunisuc2  7086  oalimcl  7685  omlimcl  7703  unblem1  8253  suppr  8418  infpr  8450  cantnfp1lem3  8615  alephnbtwn  8932  kmlem4  9013  cfsuc  9117  isf32lem5  9217  hargch  9533  xrltnsym2  12009  fzp1nel  12462  fsumsplit  14515  sumsplit  14543  phiprmpw  15528  odzdvds  15547  pcdvdsb  15620  prmreclem5  15671  ramlb  15770  pltn2lp  17016  gsumzsplit  18373  dprdcntz2  18483  lbsextlem4  19209  obselocv  20120  maducoeval2  20494  lmmo  21232  kqcldsat  21584  rnelfmlem  21803  tsmssplit  22002  itg2splitlem  23560  itg2split  23561  fsumharmonic  24783  lgsne0  25105  lgsquadlem3  25152  axtgupdim2  25415  nmounbi  27759  hatomistici  29349  eliccelico  29667  elicoelioo  29668  nn0min  29695  2sqcoprm  29775  isarchi2  29867  archiabl  29880  oddpwdc  30544  eulerpartlemsv2  30548  eulerpartlems  30550  eulerpartlemv  30554  eulerpartlemgh  30568  eulerpartlemgs2  30570  ballotlemfrcn0  30719  bnj1533  31048  bnj1204  31206  bnj1280  31214  subfacp1lem6  31293  poseq  31878  wzel  31894  nosepssdm  31961  nosupbnd1lem4  31982  nocvxminlem  32018  df3nandALT1  32521  df3nandALT2  32522  limsucncmpi  32569  unblimceq0  32623  mpnanrd  33308  relowlpssretop  33342  wl-dfnan2  33426  nninfnub  33677  atlatmstc  34924  fnwe2lem2  37938  dfxor4  38375  pm10.57  38887  limclner  40201  limsupub  40254  limsuppnflem  40260  limsupre2lem  40274  icccncfext  40418  stoweidlem14  40549  stoweidlem34  40569  stoweidlem44  40579  ldepslinc  42623  elsetrecslem  42770  alimp-no-surprise  42855
  Copyright terms: Public domain W3C validator