Theorem 3adantll3

Description: Deduction adding a conjunct to antecedent. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypothesis	3adantll3.1	|- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ta )
Assertion	3adantll3	|- ( ( ( ( ph /\ ps /\ et ) /\ ch ) /\ th ) -> ta )

Proof

Step	Hyp	Ref	Expression
1		3adantll3.1	|- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ta )
2		simpll1	|- ( ( ( ( ph /\ ps /\ et ) /\ ch ) /\ th ) -> ph )
3		simpll2	|- ( ( ( ( ph /\ ps /\ et ) /\ ch ) /\ th ) -> ps )
4	2 3	jca	|- ( ( ( ( ph /\ ps /\ et ) /\ ch ) /\ th ) -> ( ph /\ ps ) )
5		simplr	|- ( ( ( ( ph /\ ps /\ et ) /\ ch ) /\ th ) -> ch )
6		simpr	|- ( ( ( ( ph /\ ps /\ et ) /\ ch ) /\ th ) -> th )
7	4 5 6 1	syl21anc	|- ( ( ( ( ph /\ ps /\ et ) /\ ch ) /\ th ) -> ta )