Theorem ex3

Description: Apply ex to a hypothesis with a 3-right-nested conjunction antecedent, with the antecedent of the assertion being a triple conjunction rather than a 2-right-nested conjunction. (Contributed by Alan Sare, 22-Apr-2018)

	Ref	Expression
Hypothesis	ex3.1	⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) ∧ 𝜃 ) → 𝜏 )
Assertion	ex3	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) → ( 𝜃 → 𝜏 ) )

Proof

Step	Hyp	Ref	Expression
1		ex3.1	⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) ∧ 𝜃 ) → 𝜏 )
2	1	ex	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) → ( 𝜃 → 𝜏 ) )
3	2	3impa	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) → ( 𝜃 → 𝜏 ) )