Metamath Proof Explorer


Theorem anrabdioph

Description: Diophantine set builder for conjunctions. (Contributed by Stefan O'Rear, 10-Oct-2014)

Ref Expression
Assertion anrabdioph t01N|φDiophNt01N|ψDiophNt01N|φψDiophN

Proof

Step Hyp Ref Expression
1 inrab t01N|φt01N|ψ=t01N|φψ
2 diophin t01N|φDiophNt01N|ψDiophNt01N|φt01N|ψDiophN
3 1 2 eqeltrrid t01N|φDiophNt01N|ψDiophNt01N|φψDiophN