Database
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
Propositional calculus
Abbreviated conjunction and disjunction of three wff's
3mix3d
Next ⟩
3pm3.2i
Metamath Proof Explorer
Ascii
Unicode
Theorem
3mix3d
Description:
Deduction introducing triple disjunction.
(Contributed by
Scott Fenton
, 8-Jun-2011)
Ref
Expression
Hypothesis
3mixd.1
⊢
φ
→
ψ
Assertion
3mix3d
⊢
φ
→
χ
∨
θ
∨
ψ
Proof
Step
Hyp
Ref
Expression
1
3mixd.1
⊢
φ
→
ψ
2
3mix3
⊢
ψ
→
χ
∨
θ
∨
ψ
3
1
2
syl
⊢
φ
→
χ
∨
θ
∨
ψ