Metamath Proof Explorer


Theorem 3jaodan

Description: Disjunction of three antecedents (deduction). (Contributed by NM, 14-Oct-2005)

Ref Expression
Hypotheses 3jaodan.1 φ ψ χ
3jaodan.2 φ θ χ
3jaodan.3 φ τ χ
Assertion 3jaodan φ ψ θ τ χ

Proof

Step Hyp Ref Expression
1 3jaodan.1 φ ψ χ
2 3jaodan.2 φ θ χ
3 3jaodan.3 φ τ χ
4 1 ex φ ψ χ
5 2 ex φ θ χ
6 3 ex φ τ χ
7 4 5 6 3jaod φ ψ θ τ χ
8 7 imp φ ψ θ τ χ