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  3610  rspc2gv  3632  intss1  4963  fvopab3ig  7012  suppimacnv  8199  odi  8617  nndi  8661  preleqALT  9657  inf3lem2  9669  pr2neOLD  10045  zorn2lem7  10542  uzind2  12711  ssfzo12  13798  elfznelfzo  13811  injresinj  13827  suppssfz  14035  sqlecan  14248  fi1uzind  14546  cramerimplem2  22690  fiinopn  22907  uhgr0v0e  29255  0uhgrsubgr  29296  0uhgrrusgr  29596  ewlkprop  29621  umgrwwlks2on  29977  3cyclfrgrrn1  30304  3cyclfrgrrn  30305  vdgn1frgrv2  30315  dvrunz  37961  ee223  44654  afveu  47165  afv2eu  47250  lindslinindsimp2  48380  nn0sumshdiglemB  48541
  Copyright terms: Public domain W3C validator