Description: Deduction introducing two antecedents. Two applications of a1d . Deduction associated with 2a1 and 2a1i . (Contributed by BJ, 10-Aug-2020)
Ref | Expression | ||
---|---|---|---|
Hypothesis | 2a1d.1 | ||
Assertion | 2a1d |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2a1d.1 | ||
2 | 1 | a1d | |
3 | 2 | a1d |