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

Theorem imnan 422
Description: Express implication in terms of conjunction. (Contributed by NM, 9-Apr-1994.)
Assertion
Ref Expression
imnan  |-  ( (
ph  ->  -.  ps )  <->  -.  ( ph  /\  ps ) )

Proof of Theorem imnan
StepHypRef Expression
1 df-an 371 . 2  |-  ( (
ph  /\  ps )  <->  -.  ( ph  ->  -.  ps ) )
21con2bii 332 1  |-  ( (
ph  ->  -.  ps )  <->  -.  ( ph  /\  ps ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  imnani  423  iman  424  ianor  488  nan  580  pm5.17  883  pm5.16  885  dn1  957  nic-ax  1480  nic-axALT  1481  alinexa  1630  dfsb3  2065  ralinexa  2755  pssn2lp  3452  disj  3714  minel  3729  disjsn  3931  sotric  4662  ordtri1  4747  poirr2  5217  funun  5455  imadif  5488  brprcneu  5679  soisoi  6014  ordsucss  6424  ordunisuc2  6450  oalimcl  6991  omlimcl  7009  unblem1  7556  suppr  7710  cantnfp1lem3  7880  cantnfp1lem3OLD  7906  alephnbtwn  8233  kmlem4  8314  cfsuc  8418  isf32lem5  8518  hargch  8832  xrltnsym2  11107  fsumsplit  13208  sumsplit  13227  phiprmpw  13843  odzdvds  13859  pcdvdsb  13927  prmreclem5  13973  ramlb  14072  pltn2lp  15131  gsumzsplit  16409  gsumzsplitOLD  16410  dprdcntz2  16524  lbsextlem4  17219  obselocv  18128  maducoeval2  18421  lmmo  18959  kqcldsat  19281  rnelfmlem  19500  tsmssplit  19701  itg2splitlem  21201  itg2split  21202  fsumharmonic  22380  lgsne0  22647  lgsquadlem3  22670  nmounbi  24127  hatomistici  25717  eliccelico  26018  elicoelioo  26019  nn0min  26041  isarchi2  26153  archiabl  26166  oddpwdc  26689  eulerpartlemsv2  26693  eulerpartlems  26695  eulerpartlemv  26699  eulerpartlemgh  26713  eulerpartlemgs2  26715  ballotlem2  26823  ballotlemfrcn0  26864  subfacp1lem6  27025  fzp1nel  27348  poseq  27665  wzel  27712  nodenselem5  27777  nodenselem7  27779  nocvxminlem  27782  nofulllem5  27798  df3nandALT1  28194  df3nandALT2  28195  limsucncmpi  28243  nninfnub  28600  n0el  28957  fnwe2lem2  29357  pm10.57  29576  stoweidlem14  29762  stoweidlem34  29782  stoweidlem44  29792  ldepslinc  30940  alimp-no-surprise  31020  bnj1533  31732  bnj1204  31890  bnj1280  31898  atlatmstc  32804
  Copyright terms: Public domain W3C validator