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  888  pm5.16  890  dn1  966  nannan  1349  nic-ax  1493  nic-axALT  1494  alinexa  1650  dfsb3  2101  ralinexa  2895  pssn2lp  3590  disj  3853  minel  3868  disjsn  4075  sotric  4816  ordtri1  4901  poirr2  5381  funun  5620  imadif  5653  brprcneu  5849  soisoi  6209  ordsucss  6638  ordunisuc2  6664  oalimcl  7211  omlimcl  7229  unblem1  7774  suppr  7932  cantnfp1lem3  8102  cantnfp1lem3OLD  8128  alephnbtwn  8455  kmlem4  8536  cfsuc  8640  isf32lem5  8740  hargch  9054  xrltnsym2  11355  fzp1nel  11773  fsumsplit  13544  sumsplit  13565  phiprmpw  14288  odzdvds  14304  pcdvdsb  14374  prmreclem5  14420  ramlb  14519  pltn2lp  15578  gsumzsplit  16923  gsumzsplitOLD  16924  dprdcntz2  17065  lbsextlem4  17786  obselocv  18737  maducoeval2  19120  lmmo  19859  kqcldsat  20212  rnelfmlem  20431  tsmssplit  20632  itg2splitlem  22133  itg2split  22134  fsumharmonic  23319  lgsne0  23586  lgsquadlem3  23609  nmounbi  25669  hatomistici  27259  eliccelico  27566  elicoelioo  27567  nn0min  27589  2sqcoprm  27613  isarchi2  27707  archiabl  27720  oddpwdc  28271  eulerpartlemsv2  28275  eulerpartlems  28277  eulerpartlemv  28281  eulerpartlemgh  28295  eulerpartlemgs2  28297  ballotlem2  28405  ballotlemfrcn0  28446  subfacp1lem6  28607  poseq  29309  wzel  29356  nodenselem5  29421  nodenselem7  29423  nocvxminlem  29426  nofulllem5  29442  df3nandALT1  29838  df3nandALT2  29839  limsucncmpi  29886  nninfnub  30220  n0el  30576  fnwe2lem2  30973  pm10.57  31230  limclner  31611  icccncfext  31644  stoweidlem14  31750  stoweidlem34  31770  stoweidlem44  31780  ldepslinc  32980  alimp-no-surprise  33066  bnj1533  33778  bnj1204  33936  bnj1280  33944  atlatmstc  34919
  Copyright terms: Public domain W3C validator