Database
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
Propositional calculus
Abbreviated conjunction and disjunction of three wff's
3mix3i
Next ⟩
3mix1d
Metamath Proof Explorer
Ascii
Unicode
Theorem
3mix3i
Description:
Introduction in triple disjunction.
(Contributed by
Mario Carneiro
, 6-Oct-2014)
Ref
Expression
Hypothesis
3mixi.1
⊢
φ
Assertion
3mix3i
⊢
ψ
∨
χ
∨
φ
Proof
Step
Hyp
Ref
Expression
1
3mixi.1
⊢
φ
2
3mix3
⊢
φ
→
ψ
∨
χ
∨
φ
3
1
2
ax-mp
⊢
ψ
∨
χ
∨
φ