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  3454  rspc2gv  3471  intss1  4626  fvopab3ig  6420  suppimacnv  7457  odi  7813  nndi  7857  preleqALT  8676  inf3lem2  8690  pr2ne  9028  zorn2lem7  9526  uzind2  11672  ssfzo12  12769  elfznelfzo  12781  injresinj  12797  suppssfz  13001  sqlecan  13178  fi1uzind  13481  cramerimplem2  20710  fiinopn  20926  uhgr0v0e  26353  0uhgrsubgr  26394  0uhgrrusgr  26709  ewlkprop  26734  umgrwwlks2on  27105  3cyclfrgrrn1  27467  3cyclfrgrrn  27468  vdgn1frgrv2  27478  dvrunz  34085  ee223  39384  afveu  41753  lindslinindsimp2  42780  nn0sumshdiglemB  42942
  Copyright terms: Public domain W3C validator