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

Theorem imnan 412
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 361 . 2  |-  ( (
ph  /\  ps )  <->  -.  ( ph  ->  -.  ps ) )
21con2bii 323 1  |-  ( (
ph  ->  -.  ps )  <->  -.  ( ph  /\  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  imnani  413  iman  414  ianor  475  nan  564  pm5.17  859  pm5.16  861  dn1  933  nic-ax  1444  nic-axALT  1445  alinexa  1585  dfsb3  2090  ralinexa  2695  pssn2lp  3392  disj  3612  minel  3627  disjsn  3812  sotric  4471  ordtri1  4556  ordsucss  4739  ordunisuc2  4765  poirr2  5199  funun  5436  imadif  5469  brprcneu  5662  soisoi  5988  oalimcl  6740  omlimcl  6758  unblem1  7296  suppr  7407  cantnfp1lem3  7570  alephnbtwn  7886  kmlem4  7967  cfsuc  8071  isf32lem5  8171  hargch  8486  xrltnsym2  10664  fsumsplit  12461  sumsplit  12480  phiprmpw  13093  odzdvds  13109  pcdvdsb  13170  prmreclem5  13216  ramlb  13315  pltn2lp  14354  gsumzsplit  15457  dprdcntz2  15524  lbsextlem4  16161  obselocv  16879  lmmo  17367  kqcldsat  17687  rnelfmlem  17906  tsmssplit  18103  itg2splitlem  19508  itg2split  19509  fsumharmonic  20718  lgsne0  20985  lgsquadlem3  21008  nmounbi  22126  hatomistici  23714  eliccelico  23977  elicoelioo  23978  ballotlem2  24526  ballotlemfrcn0  24567  subfacp1lem6  24651  fzp1nel  24990  poseq  25278  nodenselem5  25364  nodenselem7  25366  nocvxminlem  25369  nofulllem5  25385  df3nandALT1  25861  df3nandALT2  25862  limsucncmpi  25910  nninfnub  26147  n0el  26400  fnwe2lem2  26818  pm10.57  27236  stoweidlem14  27432  stoweidlem34  27452  stoweidlem44  27462  bnj1533  28562  bnj1204  28720  bnj1280  28728  dfsb3NEW7  28973  atlatmstc  29435
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator