Description: Obsolete version of r19.29vva as of 28-Jun-2023. (Contributed by Thierry Arnoux, 26-Nov-2017) (Proof modification is discouraged.) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | r19.29vva.1 | ||
r19.29vva.2 | |||
Assertion | r19.29vvaOLD |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | r19.29vva.1 | ||
2 | r19.29vva.2 | ||
3 | 1 | ex | |
4 | 3 | ralrimiva | |
5 | 4 | ralrimiva | |
6 | 5 2 | r19.29d2r | |
7 | pm3.35 | ||
8 | 7 | ancoms | |
9 | 8 | rexlimivw | |
10 | 9 | rexlimivw | |
11 | 6 10 | syl |