Metamath Proof Explorer

Theorem 3adantlr3

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

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

Proof

Step Hyp Ref Expression
1 3adantlr3.1 
 |-  ( ( ( ph /\ ( ps /\ ch ) ) /\ th ) -> ta )
2 simpll 
 |-  ( ( ( ph /\ ( ps /\ ch /\ et ) ) /\ th ) -> ph )
3 simplr1 
 |-  ( ( ( ph /\ ( ps /\ ch /\ et ) ) /\ th ) -> ps )
4 simplr2 
 |-  ( ( ( ph /\ ( ps /\ ch /\ et ) ) /\ th ) -> ch )
5 3 4 jca 
 |-  ( ( ( ph /\ ( ps /\ ch /\ et ) ) /\ th ) -> ( ps /\ ch ) )
6 simpr 
 |-  ( ( ( ph /\ ( ps /\ ch /\ et ) ) /\ th ) -> th )
7 2 5 6 1 syl21anc 
 |-  ( ( ( ph /\ ( ps /\ ch /\ et ) ) /\ th ) -> ta )