Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005)
Ref | Expression | ||
---|---|---|---|
Hypothesis | 3adantr.1 | |
|
Assertion | 3adantr2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3adantr.1 | |
|
2 | 3simpb | |
|
3 | 2 1 | sylan2 | |