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  1481  nic-axALT  1482  alinexa  1631  dfsb3  2075  ralinexa  2882  pssn2lp  3566  disj  3828  minel  3843  disjsn  4045  sotric  4776  ordtri1  4861  poirr2  5331  funun  5569  imadif  5602  brprcneu  5793  soisoi  6129  ordsucss  6540  ordunisuc2  6566  oalimcl  7110  omlimcl  7128  unblem1  7676  suppr  7830  cantnfp1lem3  8000  cantnfp1lem3OLD  8026  alephnbtwn  8353  kmlem4  8434  cfsuc  8538  isf32lem5  8638  hargch  8952  xrltnsym2  11227  fsumsplit  13335  sumsplit  13354  phiprmpw  13970  odzdvds  13986  pcdvdsb  14054  prmreclem5  14100  ramlb  14199  pltn2lp  15259  gsumzsplit  16540  gsumzsplitOLD  16541  dprdcntz2  16659  lbsextlem4  17366  obselocv  18279  maducoeval2  18579  lmmo  19117  kqcldsat  19439  rnelfmlem  19658  tsmssplit  19859  itg2splitlem  21360  itg2split  21361  fsumharmonic  22539  lgsne0  22806  lgsquadlem3  22829  nmounbi  24329  hatomistici  25919  eliccelico  26213  elicoelioo  26214  nn0min  26236  isarchi2  26348  archiabl  26361  oddpwdc  26882  eulerpartlemsv2  26886  eulerpartlems  26888  eulerpartlemv  26892  eulerpartlemgh  26906  eulerpartlemgs2  26908  ballotlem2  27016  ballotlemfrcn0  27057  subfacp1lem6  27218  fzp1nel  27542  poseq  27859  wzel  27906  nodenselem5  27971  nodenselem7  27973  nocvxminlem  27976  nofulllem5  27992  df3nandALT1  28388  df3nandALT2  28389  limsucncmpi  28436  nninfnub  28796  n0el  29153  fnwe2lem2  29553  pm10.57  29772  stoweidlem14  29958  stoweidlem34  29978  stoweidlem44  29988  ldepslinc  31184  alimp-no-surprise  31466  bnj1533  32178  bnj1204  32336  bnj1280  32344  atlatmstc  33303
  Copyright terms: Public domain W3C validator