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  886  pm5.16  888  dn1  964  nic-ax  1490  nic-axALT  1491  alinexa  1640  dfsb3  2088  ralinexa  2916  pssn2lp  3605  disj  3867  minel  3882  disjsn  4088  sotric  4826  ordtri1  4911  poirr2  5389  funun  5628  imadif  5661  brprcneu  5857  soisoi  6210  ordsucss  6631  ordunisuc2  6657  oalimcl  7206  omlimcl  7224  unblem1  7768  suppr  7925  cantnfp1lem3  8095  cantnfp1lem3OLD  8121  alephnbtwn  8448  kmlem4  8529  cfsuc  8633  isf32lem5  8733  hargch  9047  xrltnsym2  11340  fsumsplit  13518  sumsplit  13539  phiprmpw  14158  odzdvds  14174  pcdvdsb  14244  prmreclem5  14290  ramlb  14389  pltn2lp  15449  gsumzsplit  16732  gsumzsplitOLD  16733  dprdcntz2  16873  lbsextlem4  17587  obselocv  18523  maducoeval2  18906  lmmo  19644  kqcldsat  19966  rnelfmlem  20185  tsmssplit  20386  itg2splitlem  21887  itg2split  21888  fsumharmonic  23066  lgsne0  23333  lgsquadlem3  23356  nmounbi  25364  hatomistici  26954  eliccelico  27253  elicoelioo  27254  nn0min  27276  isarchi2  27388  archiabl  27401  oddpwdc  27930  eulerpartlemsv2  27934  eulerpartlems  27936  eulerpartlemv  27940  eulerpartlemgh  27954  eulerpartlemgs2  27956  ballotlem2  28064  ballotlemfrcn0  28105  subfacp1lem6  28266  fzp1nel  28590  poseq  28907  wzel  28954  nodenselem5  29019  nodenselem7  29021  nocvxminlem  29024  nofulllem5  29040  df3nandALT1  29436  df3nandALT2  29437  limsucncmpi  29484  nninfnub  29845  n0el  30202  fnwe2lem2  30601  pm10.57  30854  limclner  31193  icccncfext  31226  stoweidlem14  31314  stoweidlem34  31334  stoweidlem44  31344  ldepslinc  32191  alimp-no-surprise  32277  bnj1533  32989  bnj1204  33147  bnj1280  33155  atlatmstc  34116
  Copyright terms: Public domain W3C validator