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  2651  2eu1v  2652  rspcebdv  3616  elpwunsn  4684  trel  5268  preddowncl  6353  predpoirr  6354  predfrirr  6355  funfvima  7250  ordsucss  7838  mapfset  8890  ac10ct  10074  ltaprlem  11084  infrelb  12253  nnmulcl  12290  ico0  13433  ioc0  13434  clwlkclwwlkfo  30028  n4cyclfrgr  30310  chlimi  31253  atcvatlem  32404  rdgssun  37379  eel12131  44733  lidldomn1  48147
  Copyright terms: Public domain W3C validator