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 ) )