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

Theorem pm2.43b 55
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 54 . 2 (𝜓 → (𝜑𝜒))
32com12 32 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:  2eu1  2640  2eu1v  2641  rspcebdv  3602  elpwunsn  4692  trel  5279  preddowncl  6345  predpoirr  6346  predfrirr  6347  funfvima  7247  ordsucss  7827  mapfset  8879  ac10ct  10077  ltaprlem  11087  infrelb  12251  nnmulcl  12288  ico0  13424  ioc0  13425  clwlkclwwlkfo  29942  n4cyclfrgr  30224  chlimi  31167  atcvatlem  32318  rdgssun  37085  eel12131  44389  lidldomn1  47608
  Copyright terms: Public domain W3C validator