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 e. ( NN0 ^m ( 1 ... N ) ) | ph } e. ( Dioph ` N ) /\ { t e. ( NN0 ^m ( 1 ... N ) ) | ps } e. ( Dioph ` N ) /\ { t e. ( NN0 ^m ( 1 ... N ) ) | ch } e. ( Dioph ` N ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | ( ph /\ ps /\ ch ) } e. ( Dioph ` N ) )

Proof

Step Hyp Ref Expression
1 df-3an
 |-  ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
2 1 rabbii
 |-  { t e. ( NN0 ^m ( 1 ... N ) ) | ( ph /\ ps /\ ch ) } = { t e. ( NN0 ^m ( 1 ... N ) ) | ( ( ph /\ ps ) /\ ch ) }
3 anrabdioph
 |-  ( ( { t e. ( NN0 ^m ( 1 ... N ) ) | ph } e. ( Dioph ` N ) /\ { t e. ( NN0 ^m ( 1 ... N ) ) | ps } e. ( Dioph ` N ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | ( ph /\ ps ) } e. ( Dioph ` N ) )
4 anrabdioph
 |-  ( ( { t e. ( NN0 ^m ( 1 ... N ) ) | ( ph /\ ps ) } e. ( Dioph ` N ) /\ { t e. ( NN0 ^m ( 1 ... N ) ) | ch } e. ( Dioph ` N ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | ( ( ph /\ ps ) /\ ch ) } e. ( Dioph ` N ) )
5 3 4 sylan
 |-  ( ( ( { t e. ( NN0 ^m ( 1 ... N ) ) | ph } e. ( Dioph ` N ) /\ { t e. ( NN0 ^m ( 1 ... N ) ) | ps } e. ( Dioph ` N ) ) /\ { t e. ( NN0 ^m ( 1 ... N ) ) | ch } e. ( Dioph ` N ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | ( ( ph /\ ps ) /\ ch ) } e. ( Dioph ` N ) )
6 2 5 eqeltrid
 |-  ( ( ( { t e. ( NN0 ^m ( 1 ... N ) ) | ph } e. ( Dioph ` N ) /\ { t e. ( NN0 ^m ( 1 ... N ) ) | ps } e. ( Dioph ` N ) ) /\ { t e. ( NN0 ^m ( 1 ... N ) ) | ch } e. ( Dioph ` N ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | ( ph /\ ps /\ ch ) } e. ( Dioph ` N ) )
7 6 3impa
 |-  ( ( { t e. ( NN0 ^m ( 1 ... N ) ) | ph } e. ( Dioph ` N ) /\ { t e. ( NN0 ^m ( 1 ... N ) ) | ps } e. ( Dioph ` N ) /\ { t e. ( NN0 ^m ( 1 ... N ) ) | ch } e. ( Dioph ` N ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | ( ph /\ ps /\ ch ) } e. ( Dioph ` N ) )