Metamath Proof Explorer

Theorem jaoded

Description: Deduction form of jao . Disjunction of antecedents. (Contributed by Alan Sare, 3-Dec-2015) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		jaoded.1	$⊢ φ \to (ψ \to χ)$
2		jaoded.2	$⊢ θ \to (τ \to χ)$
3		jaoded.3	$⊢ η \to (ψ \lor τ)$
4		jao	$⊢ (ψ \to χ) \to ((τ \to χ) \to ((ψ \lor τ) \to χ))$
5	4	3imp	$⊢ ((ψ \to χ) \land (τ \to χ) \land (ψ \lor τ)) \to χ$
6	1 2 3 5	syl3an	$⊢ (φ \land θ \land η) \to χ$