MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imnan Structured version   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  1447  nic-axALT  1448  alinexa  1588  dfsb3  2116  ralinexa  2742  pssn2lp  3440  disj  3660  minel  3675  disjsn  3860  sotric  4521  ordtri1  4606  ordsucss  4790  ordunisuc2  4816  poirr2  5250  funun  5487  imadif  5520  brprcneu  5713  soisoi  6040  oalimcl  6795  omlimcl  6813  unblem1  7351  suppr  7465  cantnfp1lem3  7628  alephnbtwn  7944  kmlem4  8025  cfsuc  8129  isf32lem5  8229  hargch  8544  xrltnsym2  10723  fsumsplit  12525  sumsplit  12544  phiprmpw  13157  odzdvds  13173  pcdvdsb  13234  prmreclem5  13280  ramlb  13379  pltn2lp  14418  gsumzsplit  15521  dprdcntz2  15588  lbsextlem4  16225  obselocv  16947  lmmo  17436  kqcldsat  17757  rnelfmlem  17976  tsmssplit  18173  itg2splitlem  19632  itg2split  19633  fsumharmonic  20842  lgsne0  21109  lgsquadlem3  21132  nmounbi  22269  hatomistici  23857  eliccelico  24132  elicoelioo  24133  isarchi2  24247  ballotlem2  24738  ballotlemfrcn0  24779  subfacp1lem6  24863  fzp1nel  25202  poseq  25520  wzel  25567  nodenselem5  25632  nodenselem7  25634  nocvxminlem  25637  nofulllem5  25653  df3nandALT1  26138  df3nandALT2  26139  limsucncmpi  26187  nninfnub  26446  n0el  26699  fnwe2lem2  27117  pm10.57  27534  stoweidlem14  27730  stoweidlem34  27750  stoweidlem44  27760  bnj1533  29160  bnj1204  29318  bnj1280  29326  dfsb3NEW7  29576  atlatmstc  30054
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