Metamath Proof Explorer


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 ψ χ φ