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  3456  rspc2gv  3474  intss1  4650  fvopab3ig  6469  suppimacnv  7510  odi  7866  nndi  7910  preleqALT  8729  inf3lem2  8743  pr2ne  9081  zorn2lem7  9579  uzind2  11720  ssfzo12  12772  elfznelfzo  12784  injresinj  12800  suppssfz  13004  sqlecan  13181  fi1uzind  13483  cramerimplem2  20772  fiinopn  20988  uhgr0v0e  26412  0uhgrsubgr  26453  0uhgrrusgr  26768  ewlkprop  26793  umgrwwlks2on  27184  3cyclfrgrrn1  27568  3cyclfrgrrn  27569  vdgn1frgrv2  27579  dvrunz  34178  ee223  39524  afveu  41904  afv2eu  41989  lindslinindsimp2  42924  nn0sumshdiglemB  43086
  Copyright terms: Public domain W3C validator