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

Theorem imnan 411
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 360 . 2  |-  ( (
ph  /\  ps )  <->  -.  ( ph  ->  -.  ps ) )
21con2bii 322 1  |-  ( (
ph  ->  -.  ps )  <->  -.  ( ph  /\  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  imnani  412  iman  413  ianor  474  nan  563  pm5.17  858  pm5.16  860  dn1  932  nic-ax  1428  nic-axALT  1429  alinexa  1565  dfsb3  1996  ralinexa  2588  pssn2lp  3277  disj  3495  minel  3510  disjsn  3693  sotric  4340  ordtri1  4425  ordsucss  4609  ordunisuc2  4635  poirr2  5067  funun  5296  imadif  5327  brprcneu  5518  soisoi  5825  oalimcl  6558  omlimcl  6576  unblem1  7109  suppr  7219  cantnfp1lem3  7382  alephnbtwn  7698  kmlem4  7779  cfsuc  7883  isf32lem5  7983  hargch  8299  xrltnsym2  10472  fsumsplit  12212  sumsplit  12231  phiprmpw  12844  odzdvds  12860  pcdvdsb  12921  prmreclem5  12967  ramlb  13066  pltn2lp  14103  gsumzsplit  15206  dprdcntz2  15273  lbsextlem4  15914  obselocv  16628  lmmo  17108  kqcldsat  17424  rnelfmlem  17647  tsmssplit  17834  itg2splitlem  19103  itg2split  19104  fsumharmonic  20305  lgsne0  20572  lgsquadlem3  20595  nmounbi  21354  hatomistici  22942  ballotlemfrcn0  23088  eliccelico  23270  elicoelioo  23271  subfacp1lem6  23716  poseq  24253  nodenselem5  24339  nodenselem7  24341  nocvxminlem  24344  nofulllem5  24360  df3nandALT1  24835  df3nandALT2  24836  limsucncmpi  24884  nninfnub  26461  n0el  26725  fnwe2lem2  27148  pm10.57  27566  stoweidlem14  27763  stoweidlem34  27783  stoweidlem44  27793  bnj1533  28884  bnj1204  29042  bnj1280  29050  a12lem2  29131  a12study  29132  a12study10  29136  a12study10n  29137  atlatmstc  29509
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 177  df-an 360
  Copyright terms: Public domain W3C validator