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  2091  ralinexa  2696  pssn2lp  3393  disj  3613  minel  3628  disjsn  3813  sotric  4472  ordtri1  4557  ordsucss  4740  ordunisuc2  4766  poirr2  5200  funun  5437  imadif  5470  brprcneu  5663  soisoi  5989  oalimcl  6741  omlimcl  6759  unblem1  7297  suppr  7408  cantnfp1lem3  7571  alephnbtwn  7887  kmlem4  7968  cfsuc  8072  isf32lem5  8172  hargch  8487  xrltnsym2  10665  fsumsplit  12462  sumsplit  12481  phiprmpw  13094  odzdvds  13110  pcdvdsb  13171  prmreclem5  13217  ramlb  13316  pltn2lp  14355  gsumzsplit  15458  dprdcntz2  15525  lbsextlem4  16162  obselocv  16880  lmmo  17368  kqcldsat  17688  rnelfmlem  17907  tsmssplit  18104  itg2splitlem  19509  itg2split  19510  fsumharmonic  20719  lgsne0  20986  lgsquadlem3  21009  nmounbi  22127  hatomistici  23715  eliccelico  23978  elicoelioo  23979  ballotlem2  24527  ballotlemfrcn0  24568  subfacp1lem6  24652  fzp1nel  24991  poseq  25279  nodenselem5  25365  nodenselem7  25367  nocvxminlem  25370  nofulllem5  25386  df3nandALT1  25862  df3nandALT2  25863  limsucncmpi  25911  nninfnub  26148  n0el  26401  fnwe2lem2  26819  pm10.57  27237  stoweidlem14  27433  stoweidlem34  27453  stoweidlem44  27463  bnj1533  28563  bnj1204  28721  bnj1280  28729  dfsb3NEW7  28974  atlatmstc  29436
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