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

Theorem imnan 424
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 373 . 2  |-  ( (
ph  /\  ps )  <->  -.  ( ph  ->  -.  ps ) )
21con2bii 334 1  |-  ( (
ph  ->  -.  ps )  <->  -.  ( ph  /\  ps ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 188    /\ wa 371
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 189  df-an 373
This theorem is referenced by:  imnani  425  iman  426  ianor  491  nan  583  pm5.17  898  pm5.16  900  dn1  976  nannan  1388  nic-ax  1555  nic-axALT  1556  alinexa  1712  dfsb3  2202  ralinexa  2838  pssn2lp  3533  disj  3804  minel  3819  disjsn  4031  sotric  4780  poirr2  5223  ordtri1  5455  funun  5623  imadif  5656  brprcneu  5856  soisoi  6217  ordsucss  6642  ordunisuc2  6668  oalimcl  7258  omlimcl  7276  unblem1  7820  suppr  7984  infpr  8016  cantnfp1lem3  8182  alephnbtwn  8499  kmlem4  8580  cfsuc  8684  isf32lem5  8784  hargch  9095  xrltnsym2  11434  fzp1nel  11875  fsumsplit  13799  sumsplit  13822  phiprmpw  14717  odzdvds  14733  odzdvdsOLD  14739  pcdvdsb  14811  prmreclem5  14857  ramlb  14970  pltn2lp  16208  gsumzsplit  17553  dprdcntz2  17664  lbsextlem4  18377  obselocv  19284  maducoeval2  19658  lmmo  20389  kqcldsat  20741  rnelfmlem  20960  tsmssplit  21159  itg2splitlem  22699  itg2split  22700  fsumharmonic  23930  lgsne0  24254  lgsquadlem3  24277  axtgupdim2  24512  nmounbi  26410  hatomistici  28008  eliccelico  28352  elicoelioo  28353  nn0min  28377  2sqcoprm  28401  isarchi2  28495  archiabl  28508  oddpwdc  29180  eulerpartlemsv2  29184  eulerpartlems  29186  eulerpartlemv  29190  eulerpartlemgh  29204  eulerpartlemgs2  29206  ballotlem2  29314  ballotlemfrcn0  29355  ballotlemfrcn0OLD  29393  bnj1533  29656  bnj1204  29814  bnj1280  29822  subfacp1lem6  29901  poseq  30484  wzel  30500  nodenselem5  30567  nodenselem7  30569  nocvxminlem  30572  nofulllem5  30588  df3nandALT1  31050  df3nandALT2  31051  limsucncmpi  31098  mpnanrd  31726  relowlpssretop  31760  wl-dfnan2  31844  nninfnub  32073  n0el  32427  atlatmstc  32879  fnwe2lem2  35903  dfxor4  36352  pm10.57  36714  limclner  37726  icccncfext  37759  stoweidlem14  37868  stoweidlem34  37889  stoweidlem44  37899  ldepslinc  40289  alimp-no-surprise  40507
  Copyright terms: Public domain W3C validator