Database
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
Propositional calculus
Abbreviated conjunction and disjunction of three wff's
simp3i
Next ⟩
simp1d
Metamath Proof Explorer
Ascii
Unicode
Theorem
simp3i
Description:
Infer a conjunct from a triple conjunction.
(Contributed by
NM
, 19-Apr-2005)
Ref
Expression
Hypothesis
3simp1i.1
⊢
φ
∧
ψ
∧
χ
Assertion
simp3i
⊢
χ
Proof
Step
Hyp
Ref
Expression
1
3simp1i.1
⊢
φ
∧
ψ
∧
χ
2
simp3
⊢
φ
∧
ψ
∧
χ
→
χ
3
1
2
ax-mp
⊢
χ