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

Theorem imnan 420
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 369 . 2  |-  ( (
ph  /\  ps )  <->  -.  ( ph  ->  -.  ps ) )
21con2bii 330 1  |-  ( (
ph  ->  -.  ps )  <->  -.  ( ph  /\  ps ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 367
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 369
This theorem is referenced by:  imnani  421  iman  422  ianor  486  nan  578  pm5.17  886  pm5.16  888  dn1  964  nannan  1346  nic-ax  1520  nic-axALT  1521  alinexa  1678  dfsb3  2129  ralinexa  2844  pssn2lp  3532  disj  3796  minel  3811  disjsn  4017  sotric  4753  ordtri1  4838  poirr2  5317  funun  5551  imadif  5584  brprcneu  5780  soisoi  6143  ordsucss  6570  ordunisuc2  6596  oalimcl  7145  omlimcl  7163  unblem1  7705  suppr  7862  cantnfp1lem3  8030  cantnfp1lem3OLD  8056  alephnbtwn  8383  kmlem4  8464  cfsuc  8568  isf32lem5  8668  hargch  8980  xrltnsym2  11283  fzp1nel  11702  fsumsplit  13583  sumsplit  13604  phiprmpw  14327  odzdvds  14343  pcdvdsb  14413  prmreclem5  14459  ramlb  14558  pltn2lp  15735  gsumzsplit  17080  gsumzsplitOLD  17081  dprdcntz2  17218  lbsextlem4  17939  obselocv  18869  maducoeval2  19246  lmmo  19986  kqcldsat  20338  rnelfmlem  20557  tsmssplit  20758  itg2splitlem  22259  itg2split  22260  fsumharmonic  23477  lgsne0  23744  lgsquadlem3  23767  axtgupdim2  24007  nmounbi  25829  hatomistici  27418  eliccelico  27771  elicoelioo  27772  nn0min  27794  2sqcoprm  27818  isarchi2  27912  archiabl  27925  oddpwdc  28512  eulerpartlemsv2  28516  eulerpartlems  28518  eulerpartlemv  28522  eulerpartlemgh  28536  eulerpartlemgs2  28538  ballotlem2  28646  ballotlemfrcn0  28687  subfacp1lem6  28854  poseq  29534  wzel  29581  nodenselem5  29646  nodenselem7  29648  nocvxminlem  29651  nofulllem5  29667  df3nandALT1  30051  df3nandALT2  30052  limsucncmpi  30099  wl-dfnan2  30172  nninfnub  30446  n0el  30802  fnwe2lem2  31199  pm10.57  31480  limclner  31858  icccncfext  31891  stoweidlem14  31997  stoweidlem34  32017  stoweidlem44  32027  ldepslinc  33345  alimp-no-surprise  33565  bnj1533  34292  bnj1204  34450  bnj1280  34458  atlatmstc  35492  dfxor4  38294
  Copyright terms: Public domain W3C validator