This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 3jaao

Description: Inference conjoining and disjoining the antecedents of three implications. (Contributed by Jeff Hankins, 15-Aug-2009) (Proof shortened by Andrew Salmon, 13-May-2011)

	Ref	Expression
Hypotheses	3jaao.1	$⊢ φ \to (ψ \to χ)$
	3jaao.2	$⊢ θ \to (τ \to χ)$
	3jaao.3	$⊢ η \to (ζ \to χ)$
Assertion	3jaao	$⊢ (φ \land θ \land η) \to ((ψ \lor τ \lor ζ) \to χ)$

Proof

Step	Hyp	Ref	Expression
1		3jaao.1	$⊢ φ \to (ψ \to χ)$
2		3jaao.2	$⊢ θ \to (τ \to χ)$
3		3jaao.3	$⊢ η \to (ζ \to χ)$
4	1	3ad2ant1	$⊢ (φ \land θ \land η) \to (ψ \to χ)$
5	2	3ad2ant2	$⊢ (φ \land θ \land η) \to (τ \to χ)$
6	3	3ad2ant3	$⊢ (φ \land θ \land η) \to (ζ \to χ)$
7	4 5 6	3jaod	$⊢ (φ \land θ \land η) \to ((ψ \lor τ \lor ζ) \to χ)$