Metamath Proof Explorer


Theorem 3anrabdioph

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

Ref Expression
Assertion 3anrabdioph t 0 1 N | φ Dioph N t 0 1 N | ψ Dioph N t 0 1 N | χ Dioph N t 0 1 N | φ ψ χ Dioph N

Proof

Step Hyp Ref Expression
1 df-3an φ ψ χ φ ψ χ
2 1 rabbii t 0 1 N | φ ψ χ = t 0 1 N | φ ψ χ
3 anrabdioph t 0 1 N | φ Dioph N t 0 1 N | ψ Dioph N t 0 1 N | φ ψ Dioph N
4 anrabdioph t 0 1 N | φ ψ Dioph N t 0 1 N | χ Dioph N t 0 1 N | φ ψ χ Dioph N
5 3 4 sylan t 0 1 N | φ Dioph N t 0 1 N | ψ Dioph N t 0 1 N | χ Dioph N t 0 1 N | φ ψ χ Dioph N
6 2 5 eqeltrid t 0 1 N | φ Dioph N t 0 1 N | ψ Dioph N t 0 1 N | χ Dioph N t 0 1 N | φ ψ χ Dioph N
7 6 3impa t 0 1 N | φ Dioph N t 0 1 N | ψ Dioph N t 0 1 N | χ Dioph N t 0 1 N | φ ψ χ Dioph N