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	|- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ta )
Assertion	ex3	|- ( ( ph /\ ps /\ ch ) -> ( th -> ta ) )

Proof

Step	Hyp	Ref	Expression
1		ex3.1	|- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ta )
2	1	ex	|- ( ( ( ph /\ ps ) /\ ch ) -> ( th -> ta ) )
3	2	3impa	|- ( ( ph /\ ps /\ ch ) -> ( th -> ta ) )