Metamath Proof Explorer


Theorem mnuprss2d

Description: Special case of mnuprssd . (Contributed by Rohan Ridenour, 13-Aug-2023)

Ref Expression
Hypotheses mnuprss2d.1 M = k | l k 𝒫 l k m n k 𝒫 l n p l q k p q q m r m p r r n
mnuprss2d.2 φ U M
mnuprss2d.3 φ C U
mnuprss2d.4 A C
mnuprss2d.5 B C
Assertion mnuprss2d φ A B U

Proof

Step Hyp Ref Expression
1 mnuprss2d.1 M = k | l k 𝒫 l k m n k 𝒫 l n p l q k p q q m r m p r r n
2 mnuprss2d.2 φ U M
3 mnuprss2d.3 φ C U
4 mnuprss2d.4 A C
5 mnuprss2d.5 B C
6 4 a1i φ A C
7 5 a1i φ B C
8 1 2 3 6 7 mnuprssd φ A B U