Metamath Proof Explorer


Theorem adantl3r

Description: Deduction adding 1 conjunct to antecedent. (Contributed by Alan Sare, 17-Oct-2017)

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

Proof

Step Hyp Ref Expression
1 adantl3r.1
 |-  ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ta )
2 id
 |-  ( ( ph /\ ps ) -> ( ph /\ ps ) )
3 2 adantlr
 |-  ( ( ( ph /\ et ) /\ ps ) -> ( ph /\ ps ) )
4 3 1 sylanl1
 |-  ( ( ( ( ( ph /\ et ) /\ ps ) /\ ch ) /\ th ) -> ta )