MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.43b Unicode version

Theorem pm2.43b 50
Description: Inference absorbing redundant antecedent. (Contributed by NM, 31-Oct-1995.)
Hypothesis
Ref Expression
pm2.43b.1
Assertion
Ref Expression
pm2.43b

Proof of Theorem pm2.43b
StepHypRef Expression
1 pm2.43b.1 . . 3
21pm2.43a 49 . 2
32com12 31 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4
This theorem is referenced by:  2eu1  2376  elpwunsn  4070  trel  4552  trss  4554  funfvima  6147  ordsucss  6653  ac10ct  8436  ltaprlem  9443  nnmulcl  10584  ico0  11604  ioc0  11605  clwlkfoclwwlk  24845  n4cyclfrgra  25018  vdgn0frgrav2  25024  chlimi  26152  atcvatlem  27304  preddowncl  29276  predpoirr  29277  predfrirr  29278  usgvincvad  32404  usgvincvadALT  32407  lidldomn1  32727  eel12131  33506  eel32131  33509
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
  Copyright terms: Public domain W3C validator