Database
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
Propositional calculus
Logical conjunction
anidms
Next ⟩
imdistan
Metamath Proof Explorer
Ascii
Unicode
Theorem
anidms
Description:
Inference from idempotent law for conjunction.
(Contributed by
NM
, 15-Jun-1994)
Ref
Expression
Hypothesis
anidms.1
⊢
φ
∧
φ
→
ψ
Assertion
anidms
⊢
φ
→
ψ
Proof
Step
Hyp
Ref
Expression
1
anidms.1
⊢
φ
∧
φ
→
ψ
2
1
ex
⊢
φ
→
φ
→
ψ
3
2
pm2.43i
⊢
φ
→
ψ