Metamath Proof Explorer

Theorem a2and

Description: Deduction distributing a conjunction as embedded antecedent. (Contributed by AV, 25-Oct-2019) (Proof shortened by Wolf Lammen, 19-Jan-2020)

		Ref	Expression
	Hypotheses	a2and.1	$⊢ φ \to ((ψ \land ρ) \to (τ \to θ))$
		a2and.2	$⊢ φ \to ((ψ \land ρ) \to χ)$
	Assertion	a2and	$⊢ φ \to (((ψ \land χ) \to τ) \to ((ψ \land ρ) \to θ))$

Proof

Step	Hyp	Ref	Expression
1		a2and.1	$⊢ φ \to ((ψ \land ρ) \to (τ \to θ))$
2		a2and.2	$⊢ φ \to ((ψ \land ρ) \to χ)$
3	2	expd	$⊢ φ \to (ψ \to (ρ \to χ))$
4	3	imdistand	$⊢ φ \to ((ψ \land ρ) \to (ψ \land χ))$
5		imim1	$⊢ ((ψ \land χ) \to τ) \to ((τ \to θ) \to ((ψ \land χ) \to θ))$
6	5	com3l	$⊢ (τ \to θ) \to ((ψ \land χ) \to (((ψ \land χ) \to τ) \to θ))$
7	1 4 6	syl6c	$⊢ φ \to ((ψ \land ρ) \to (((ψ \land χ) \to τ) \to θ))$
8	7	com23	$⊢ φ \to (((ψ \land χ) \to τ) \to ((ψ \land ρ) \to θ))$