Metamath Proof Explorer

Theorem pm2.43

Description: Absorption of redundant antecedent. Also called the "Contraction" or "Hilbert" axiom. Theorem *2.43 of WhiteheadRussell p. 106. (Contributed by NM, 10-Jan-1993) (Proof shortened by Mel L. O'Cat, 15-Aug-2004)

Ref Expression
Assertion pm2.43 φ φ ψ φ ψ


Step Hyp Ref Expression
1 pm2.27 φ φ ψ ψ
2 1 a2i φ φ ψ φ ψ