Metamath Proof Explorer


Theorem pm3.4

Description: Conjunction implies implication. Theorem *3.4 of WhiteheadRussell p. 113. (Contributed by NM, 31-Jul-1995)

Ref Expression
Assertion pm3.4 φ ψ φ ψ

Proof

Step Hyp Ref Expression
1 simpr φ ψ ψ
2 1 a1d φ ψ φ ψ