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  3608  rspc2gv  3629  intss1  4882  fvopab3ig  6757  suppimacnv  7830  odi  8194  nndi  8238  preleqALT  9068  inf3lem2  9080  pr2ne  9419  zorn2lem7  9912  uzind2  12063  ssfzo12  13118  elfznelfzo  13130  injresinj  13146  suppssfz  13350  sqlecan  13559  fi1uzind  13843  cramerimplem2  21221  fiinopn  21437  uhgr0v0e  26947  0uhgrsubgr  26988  0uhgrrusgr  27287  ewlkprop  27312  umgrwwlks2on  27663  3cyclfrgrrn1  27991  3cyclfrgrrn  27992  vdgn1frgrv2  28002  dvrunz  35113  ee223  40845  afveu  43229  afv2eu  43314  lindslinindsimp2  44446  nn0sumshdiglemB  44608
  Copyright terms: Public domain W3C validator