Metamath Proof Explorer

Theorem 3adantll2

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

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

Proof

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