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  2105  ralinexa  2711  pssn2lp  3408  disj  3628  minel  3643  disjsn  3828  sotric  4489  ordtri1  4574  ordsucss  4757  ordunisuc2  4783  poirr2  5217  funun  5454  imadif  5487  brprcneu  5680  soisoi  6007  oalimcl  6762  omlimcl  6780  unblem1  7318  suppr  7429  cantnfp1lem3  7592  alephnbtwn  7908  kmlem4  7989  cfsuc  8093  isf32lem5  8193  hargch  8508  xrltnsym2  10687  fsumsplit  12488  sumsplit  12507  phiprmpw  13120  odzdvds  13136  pcdvdsb  13197  prmreclem5  13243  ramlb  13342  pltn2lp  14381  gsumzsplit  15484  dprdcntz2  15551  lbsextlem4  16188  obselocv  16910  lmmo  17398  kqcldsat  17718  rnelfmlem  17937  tsmssplit  18134  itg2splitlem  19593  itg2split  19594  fsumharmonic  20803  lgsne0  21070  lgsquadlem3  21093  nmounbi  22230  hatomistici  23818  eliccelico  24093  elicoelioo  24094  isarchi2  24208  ballotlem2  24699  ballotlemfrcn0  24740  subfacp1lem6  24824  fzp1nel  25163  poseq  25467  nodenselem5  25553  nodenselem7  25555  nocvxminlem  25558  nofulllem5  25574  df3nandALT1  26050  df3nandALT2  26051  limsucncmpi  26099  nninfnub  26345  n0el  26598  fnwe2lem2  27016  pm10.57  27434  stoweidlem14  27630  stoweidlem34  27650  stoweidlem44  27660  bnj1533  28929  bnj1204  29087  bnj1280  29095  dfsb3NEW7  29340  atlatmstc  29802
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