MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imnan Structured 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  897  pm5.16  899  dn1  975  nannan  1385  nic-ax  1553  nic-axALT  1554  alinexa  1709  dfsb3  2169  ralinexa  2878  pssn2lp  3567  disj  3834  minel  3849  disjsn  4058  sotric  4798  poirr2  5241  ordtri1  5473  funun  5641  imadif  5674  brprcneu  5872  soisoi  6232  ordsucss  6657  ordunisuc2  6683  oalimcl  7267  omlimcl  7285  unblem1  7827  suppr  7991  infpr  8023  cantnfp1lem3  8188  alephnbtwn  8504  kmlem4  8585  cfsuc  8689  isf32lem5  8789  hargch  9100  xrltnsym2  11439  fzp1nel  11880  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  19283  maducoeval2  19657  lmmo  20388  kqcldsat  20740  rnelfmlem  20959  tsmssplit  21158  itg2splitlem  22698  itg2split  22699  fsumharmonic  23929  lgsne0  24253  lgsquadlem3  24276  axtgupdim2  24511  nmounbi  26409  hatomistici  28007  eliccelico  28359  elicoelioo  28360  nn0min  28385  2sqcoprm  28409  isarchi2  28503  archiabl  28516  oddpwdc  29189  eulerpartlemsv2  29193  eulerpartlems  29195  eulerpartlemv  29199  eulerpartlemgh  29213  eulerpartlemgs2  29215  ballotlem2  29323  ballotlemfrcn0  29364  ballotlemfrcn0OLD  29402  bnj1533  29665  bnj1204  29823  bnj1280  29831  subfacp1lem6  29910  poseq  30492  wzel  30508  nodenselem5  30573  nodenselem7  30575  nocvxminlem  30578  nofulllem5  30594  df3nandALT1  31056  df3nandALT2  31057  limsucncmpi  31104  mpnanrd  31691  relowlpssretop  31725  wl-dfnan2  31809  nninfnub  32038  n0el  32393  atlatmstc  32848  fnwe2lem2  35873  dfxor4  36262  pm10.57  36622  limclner  37596  icccncfext  37629  stoweidlem14  37738  stoweidlem34  37759  stoweidlem44  37769  ldepslinc  39646  alimp-no-surprise  39864
  Copyright terms: Public domain W3C validator