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