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 )