Description: mnussd with arguments provided with an existential quantifier. (Contributed by Rohan Ridenour, 13-Aug-2023)
Ref | Expression | ||
---|---|---|---|
Hypotheses | mnuss2d.1 | ||
mnuss2d.2 | |||
mnuss2d.3 | |||
Assertion | mnuss2d |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mnuss2d.1 | ||
2 | mnuss2d.2 | ||
3 | mnuss2d.3 | ||
4 | 2 | adantr | |
5 | simprl | ||
6 | simprr | ||
7 | 1 4 5 6 | mnussd | |
8 | 3 7 | rexlimddv |