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

Theorem pm2.43a 49
Description: Inference absorbing redundant antecedent. (Contributed by NM, 7-Nov-1995.) (Proof shortened by Mel L. O'Cat, 28-Nov-2008.)
Hypothesis
Ref Expression
pm2.43a.1
Assertion
Ref Expression
pm2.43a

Proof of Theorem pm2.43a
StepHypRef Expression
1 id 22 . 2
2 pm2.43a.1 . 2
31, 2mpid 41 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4
This theorem is referenced by:  pm2.43b  50  rspc  3204  intss1  4301  fvopab3ig  5953  suppimacnv  6929  odi  7247  nndi  7291  inf3lem2  8067  pr2ne  8404  zorn2lem7  8903  uzind2  10980  uzindOLD  10982  ssfzo12  11905  elfznelfzo  11915  injresinj  11926  suppssfz  12100  sqlecan  12274  brfi1uzind  12532  cramerimplem2  19186  fiinopn  19410  bwthOLD  19911  usgraedg4  24387  wlkdvspthlem  24609  usgrcyclnl1  24640  3cyclfrgrarn1  25012  vdn0frgrav2  25023  vdn1frgrav2  25025  vdgn1frgrav2  25026  numclwlk1lem2foa  25091  dvrunz  25435  afveu  32238  lindslinindsimp2  33064  ee223  33420
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
  Copyright terms: Public domain W3C validator