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

Theorem imnan 429
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 378 . 2  |-  ( (
ph  /\  ps )  <->  -.  ( ph  ->  -.  ps ) )
21con2bii 339 1  |-  ( (
ph  ->  -.  ps )  <->  -.  ( ph  /\  ps ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 189    /\ wa 376
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 190  df-an 378
This theorem is referenced by:  imnani  430  iman  431  ianor  496  nan  590  pm5.17  905  pm5.16  907  dn1  977  nannan  1416  nic-ax  1564  nic-axALT  1565  alinexa  1721  dfsb3  2223  ralinexa  2838  pssn2lp  3520  disj  3809  minel  3824  disjsn  4023  sotric  4786  poirr2  5230  ordtri1  5463  funun  5631  imadif  5668  brprcneu  5872  soisoi  6237  ordsucss  6664  ordunisuc2  6690  oalimcl  7279  omlimcl  7297  unblem1  7841  suppr  8005  infpr  8037  cantnfp1lem3  8203  alephnbtwn  8520  kmlem4  8601  cfsuc  8705  isf32lem5  8805  hargch  9116  xrltnsym2  11460  fzp1nel  11904  fsumsplit  13883  sumsplit  13906  phiprmpw  14803  odzdvds  14819  odzdvdsOLD  14825  pcdvdsb  14897  prmreclem5  14943  ramlb  15056  pltn2lp  16293  gsumzsplit  17638  dprdcntz2  17749  lbsextlem4  18462  obselocv  19368  maducoeval2  19742  lmmo  20473  kqcldsat  20825  rnelfmlem  21045  tsmssplit  21244  itg2splitlem  22785  itg2split  22786  fsumharmonic  24016  lgsne0  24340  lgsquadlem3  24363  axtgupdim2  24598  nmounbi  26498  hatomistici  28096  eliccelico  28434  elicoelioo  28435  nn0min  28459  2sqcoprm  28483  isarchi2  28576  archiabl  28589  oddpwdc  29260  eulerpartlemsv2  29264  eulerpartlems  29266  eulerpartlemv  29270  eulerpartlemgh  29284  eulerpartlemgs2  29286  ballotlem2  29394  ballotlemfrcn0  29435  ballotlemfrcn0OLD  29473  bnj1533  29735  bnj1204  29893  bnj1280  29901  subfacp1lem6  29980  poseq  30562  wzel  30578  nodenselem5  30645  nodenselem7  30647  nocvxminlem  30650  nofulllem5  30666  df3nandALT1  31128  df3nandALT2  31129  limsucncmpi  31176  mpnanrd  31803  relowlpssretop  31837  wl-dfnan2  31921  nninfnub  32144  n0el  32497  atlatmstc  32956  fnwe2lem2  35980  dfxor4  36429  pm10.57  36790  limclner  37829  icccncfext  37862  stoweidlem14  37986  stoweidlem34  38007  stoweidlem44  38017  ldepslinc  40810  alimp-no-surprise  41026
  Copyright terms: Public domain W3C validator