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  3559  rspc2gv  3580  intss1  4853  fvopab3ig  6741  suppimacnv  7824  odi  8188  nndi  8232  preleqALT  9064  inf3lem2  9076  pr2ne  9416  zorn2lem7  9913  uzind2  12063  ssfzo12  13125  elfznelfzo  13137  injresinj  13153  suppssfz  13357  sqlecan  13567  fi1uzind  13851  cramerimplem2  21289  fiinopn  21506  uhgr0v0e  27028  0uhgrsubgr  27069  0uhgrrusgr  27368  ewlkprop  27393  umgrwwlks2on  27743  3cyclfrgrrn1  28070  3cyclfrgrrn  28071  vdgn1frgrv2  28081  dvrunz  35392  ee223  41338  afveu  43707  afv2eu  43792  lindslinindsimp2  44870  nn0sumshdiglemB  45032
  Copyright terms: Public domain W3C validator