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  3600  rspc2gv  3620  intss1  4966  fvopab3ig  6990  suppimacnv  8154  odi  8575  nndi  8619  preleqALT  9608  inf3lem2  9620  pr2neOLD  9996  zorn2lem7  10493  uzind2  12651  ssfzo12  13721  elfznelfzo  13733  injresinj  13749  suppssfz  13955  sqlecan  14169  fi1uzind  14454  cramerimplem2  22168  fiinopn  22385  uhgr0v0e  28475  0uhgrsubgr  28516  0uhgrrusgr  28815  ewlkprop  28840  umgrwwlks2on  29191  3cyclfrgrrn1  29518  3cyclfrgrrn  29519  vdgn1frgrv2  29529  dvrunz  36760  ee223  43328  afveu  45796  afv2eu  45881  lindslinindsimp2  47046  nn0sumshdiglemB  47208
  Copyright terms: Public domain W3C validator