Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004) (Proof shortened by Wolf Lammen, 4-Dec-2012)
Ref | Expression | ||
---|---|---|---|
Hypothesis | adantr2.1 | |- ( ( ph /\ ( ps /\ ch ) ) -> th ) |
|
Assertion | adantrlr | |- ( ( ph /\ ( ( ps /\ ta ) /\ ch ) ) -> th ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | adantr2.1 | |- ( ( ph /\ ( ps /\ ch ) ) -> th ) |
|
2 | simpl | |- ( ( ps /\ ta ) -> ps ) |
|
3 | 2 1 | sylanr1 | |- ( ( ph /\ ( ( ps /\ ta ) /\ ch ) ) -> th ) |