Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006) (Proof shortened by Wolf Lammen, 25-Jun-2022)
Ref | Expression | ||
---|---|---|---|
Hypothesis | ad4ant3.1 | |- ( ( ph /\ ps /\ ch ) -> th ) |
|
Assertion | 3adant3l | |- ( ( ph /\ ps /\ ( ta /\ ch ) ) -> th ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ad4ant3.1 | |- ( ( ph /\ ps /\ ch ) -> th ) |
|
2 | simpr | |- ( ( ta /\ ch ) -> ch ) |
|
3 | 2 1 | syl3an3 | |- ( ( ph /\ ps /\ ( ta /\ ch ) ) -> th ) |