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

Theorem pm2.43a 54
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 44 1 (𝜓 → (𝜑𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  pm2.43b  55  rspc  3298  rspc2gv  3316  intss1  4483  fvopab3ig  6265  suppimacnv  7291  odi  7644  nndi  7688  inf3lem2  8511  pr2ne  8813  zorn2lem7  9309  uzind2  11455  ssfzo12  12545  elfznelfzo  12557  injresinj  12572  suppssfz  12777  sqlecan  12954  fi1uzind  13262  fi1uzindOLD  13268  cramerimplem2  20471  fiinopn  20687  uhgr0v0e  26111  0uhgrsubgr  26152  0uhgrrusgr  26455  ewlkprop  26480  umgrwwlks2on  26831  3cyclfrgrrn1  27129  3cyclfrgrrn  27130  vdgn1frgrv2  27140  numclwlk1lem2foa  27195  dvrunz  33724  ee223  38679  afveu  40996  lindslinindsimp2  42017  nn0sumshdiglemB  42179
  Copyright terms: Public domain W3C validator