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